Left Termination proof of /tmp/tmplkEfHQ/binary3.pl

Left Termination of the query pattern
times(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇒, 389 ms)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇒, 496 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 7 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 5 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇒, 0 ms)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔, 0 ms)

        ↳34 YES

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔, 0 ms)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇒, 0 ms)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔, 0 ms)

        ↳41 YES

(0) Obligation:

Clauses:

add(b, b, b).
add(X, b, X) :- binaryZ(X).
add(b, Y, Y) :- binaryZ(Y).
add(X, Y, Z) :- addz(X, Y, Z).
addx(one(X), b, one(X)) :- binary(X).
addx(zero(X), b, zero(X)) :- binaryZ(X).
addx(X, Y, Z) :- addz(X, Y, Z).
addy(b, one(Y), one(Y)) :- binary(Y).
addy(b, zero(Y), zero(Y)) :- binaryZ(Y).
addy(X, Y, Z) :- addz(X, Y, Z).
addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z).
addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z).
addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z).
addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z).
addc(b, b, one(b)).
addc(X, b, Z) :- succZ(X, Z).
addc(b, Y, Z) :- succZ(Y, Z).
addc(X, Y, Z) :- addC(X, Y, Z).
addX(zero(X), b, one(X)) :- binaryZ(X).
addX(one(X), b, zero(Z)) :- succ(X, Z).
addX(X, Y, Z) :- addC(X, Y, Z).
addY(b, zero(Y), one(Y)) :- binaryZ(Y).
addY(b, one(Y), zero(Z)) :- succ(Y, Z).
addY(X, Y, Z) :- addC(X, Y, Z).
addC(zero(X), zero(Y), one(Z)) :- addz(X, Y, Z).
addC(zero(X), one(Y), zero(Z)) :- addX(X, Y, Z).
addC(one(X), zero(Y), zero(Z)) :- addY(X, Y, Z).
addC(one(X), one(Y), one(Z)) :- addc(X, Y, Z).
binary(b).
binary(zero(X)) :- binaryZ(X).
binary(one(X)) :- binary(X).
binaryZ(zero(X)) :- binaryZ(X).
binaryZ(one(X)) :- binary(X).
succ(b, one(b)).
succ(zero(X), one(X)) :- binaryZ(X).
succ(one(X), zero(Z)) :- succ(X, Z).
succZ(zero(X), one(X)) :- binaryZ(X).
succZ(one(X), zero(Z)) :- succ(X, Z).
times(one(b), X, X).
times(zero(R), S, zero(RS)) :- times(R, S, RS).
times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS)).

Query: times(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: times(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: times(T1, T2, T3), SCOPE: 1, CLAUSE: 38 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 39 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 39 | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: times(T1, T2, T3), SCOPE: 1, CLAUSE: 39 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground\nX2 is free\ntimes(T1, T2, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: times(one(b), T5, T3), SCOPE: 1, CLAUSE: 39 | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(times(b, T8, X12), add(T8, zero(X12), T10))\n\nT8 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 38 | ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 39 | ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 39 | ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: times(T14, T15, T17) | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground\nX2 is free\nX23 is free\nX24 is free\nX25 is free\ntimes(T1, T2, T3) !=? times(one(b), X2, X2)\ntimes(T1, T2, T3) !=? times(zero(X23), X24, zero(X25))", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: times(T14, T15, T17), SCOPE: 3, CLAUSE: 38 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 39 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: times(T14, T15, T17), SCOPE: 3, CLAUSE: 38\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: times(T14, T15, T17), SCOPE: 3, CLAUSE: 39 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: times(T14, T15, T17), SCOPE: 3, CLAUSE: 39\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: times(T35, T36, T38)\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: times(T14, T15, T17), SCOPE: 3, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(times(T53, T54, X65), add(T54, zero(X65), T56))\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="C: times(T53, T54, X65)\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="B: add(T54, zero(T59), T56)\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: times(T53, T54, X65), SCOPE: 4, CLAUSE: 38 | times(T53, T54, X65), SCOPE: 4, CLAUSE: 39 | times(T53, T54, X65), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: times(T53, T54, X65), SCOPE: 4, CLAUSE: 38\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: times(T53, T54, X65), SCOPE: 4, CLAUSE: 39 | times(T53, T54, X65), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: times(T53, T54, X65), SCOPE: 4, CLAUSE: 39\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: times(T53, T54, X65), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: times(T75, T76, X94)\n\nT75 is ground\nT76 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(times(T83, T84, X109), add(T84, zero(X109), X110))\n\nT83 is ground\nT84 is ground\nX110 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: times(T83, T84, X109)\n\nT83 is ground\nT84 is ground\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: add(T84, zero(T87), X110)\n\nT84 is ground\nT87 is ground\nX110 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 0 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 1 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 1 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: binaryZ(zero(T95))\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: binaryZ(zero(T95)), SCOPE: 6, CLAUSE: 31 | binaryZ(zero(T95)), SCOPE: 6, CLAUSE: 32\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: binaryZ(zero(T95)), SCOPE: 6, CLAUSE: 31\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: binaryZ(zero(T95)), SCOPE: 6, CLAUSE: 32\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="D: binaryZ(T103)\n\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: binaryZ(T103), SCOPE: 7, CLAUSE: 31 | binaryZ(T103), SCOPE: 7, CLAUSE: 32\n\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: binaryZ(T103), SCOPE: 7, CLAUSE: 31\n\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: binaryZ(T103), SCOPE: 7, CLAUSE: 32\n\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: binaryZ(T109)\n\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="G: binary(T113)\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: binary(T113), SCOPE: 8, CLAUSE: 28 | binary(T113), SCOPE: 8, CLAUSE: 29 | binary(T113), SCOPE: 8, CLAUSE: 30\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: binary(T113), SCOPE: 8, CLAUSE: 28\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: binary(T113), SCOPE: 8, CLAUSE: 29 | binary(T113), SCOPE: 8, CLAUSE: 30\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: binary(T113), SCOPE: 8, CLAUSE: 29\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: binary(T113), SCOPE: 8, CLAUSE: 30\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: binaryZ(T118)\n\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: binary(T122)\n\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: addz(T133, zero(T134), T136)\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 10 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 11 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 12 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 13\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 10\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 11 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 12 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 13\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="E: addz(T152, T153, T155)\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 10 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 11 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 12 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 13\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 10\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 11 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 12 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 13\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: addz(T171, T172, T174)\n\nT171 is ground\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 11\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 12 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 13\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: addx(T190, T191, T193)\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 4 | addx(T190, T191, T193), SCOPE: 11, CLAUSE: 5 | addx(T190, T191, T193), SCOPE: 11, CLAUSE: 6\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 4\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 5 | addx(T190, T191, T193), SCOPE: 11, CLAUSE: 6\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: binary(T199)\n\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 5\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 6\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: binaryZ(T204)\n\nT204 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: addz(T216, T217, T219)\n\nT216 is ground\nT217 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 12\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 13\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="F: addy(T235, T236, T238)\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 7 | addy(T235, T236, T238), SCOPE: 12, CLAUSE: 8 | addy(T235, T236, T238), SCOPE: 12, CLAUSE: 9\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 7\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 8 | addy(T235, T236, T238), SCOPE: 12, CLAUSE: 9\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: binary(T244)\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 8\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 9\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: binaryZ(T249)\n\nT249 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: addz(T261, T262, T264)\n\nT261 is ground\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="H: addc(T274, T275, T277)\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 14 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 15 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 16 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 17\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 14\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 15 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 16 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 17\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 15\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 16 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 17\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="J: succZ(T286, T288)\n\nT286 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: succZ(T286, T288), SCOPE: 14, CLAUSE: 36 | succZ(T286, T288), SCOPE: 14, CLAUSE: 37\n\nT286 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: succZ(T286, T288), SCOPE: 14, CLAUSE: 36\n\nT286 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: succZ(T286, T288), SCOPE: 14, CLAUSE: 37\n\nT286 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: binaryZ(T294)\n\nT294 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="I: succ(T300, T302)\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: succ(T300, T302), SCOPE: 15, CLAUSE: 33 | succ(T300, T302), SCOPE: 15, CLAUSE: 34 | succ(T300, T302), SCOPE: 15, CLAUSE: 35\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: succ(T300, T302), SCOPE: 15, CLAUSE: 33\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: succ(T300, T302), SCOPE: 15, CLAUSE: 34 | succ(T300, T302), SCOPE: 15, CLAUSE: 35\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: succ(T300, T302), SCOPE: 15, CLAUSE: 34\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: succ(T300, T302), SCOPE: 15, CLAUSE: 35\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: binaryZ(T307)\n\nT307 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: succ(T313, T315)\n\nT313 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 16\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 17\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: succZ(T324, T326)\n\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="K: addC(T338, T339, T341)\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 24 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 25 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 26 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 27\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 24\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 25 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 26 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 27\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: addz(T357, T358, T360)\n\nT357 is ground\nT358 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 25\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 26 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 27\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: addX(T376, T377, T379)\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 18 | addX(T376, T377, T379), SCOPE: 17, CLAUSE: 19 | addX(T376, T377, T379), SCOPE: 17, CLAUSE: 20\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 18\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 19 | addX(T376, T377, T379), SCOPE: 17, CLAUSE: 20\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: binaryZ(T385)\n\nT385 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 19\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 20\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: succ(T395, T397)\n\nT395 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: addC(T408, T409, T411)\n\nT408 is ground\nT409 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 26\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 27\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: addY(T427, T428, T430)\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 21 | addY(T427, T428, T430), SCOPE: 18, CLAUSE: 22 | addY(T427, T428, T430), SCOPE: 18, CLAUSE: 23\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 21\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 22 | addY(T427, T428, T430), SCOPE: 18, CLAUSE: 23\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: binaryZ(T436)\n\nT436 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 22\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 23\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: succ(T446, T448)\n\nT446 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: addC(T459, T460, T462)\n\nT459 is ground\nT460 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: addc(T472, T473, T475)\n\nT472 is ground\nT473 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 12 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 13\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 12\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 13\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: addy(T489, T490, T492)\n\nT489 is ground\nT490 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(times(T498, T499, X506), add(T499, zero(X506), T501))\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 38 | ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 39 | ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 40\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 38\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 39 | ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 40\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: add(T506, zero(T506), T501)\n\nT506 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 39\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 40\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(times(T515, T516, X531), add(T516, zero(zero(X531)), T501))\n\nT515 is ground\nT516 is ground\nX531 is free", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: times(T515, T516, X531)\n\nT515 is ground\nT516 is ground\nX531 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: add(T516, zero(zero(T519)), T501)\n\nT516 is ground\nT519 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(','(times(T526, T527, X548), add(T527, zero(X548), X549)), add(T527, zero(X549), T501))\n\nT526 is ground\nT527 is ground\nX549 is free\nX548 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: times(T526, T527, X548)\n\nT526 is ground\nT527 is ground\nX548 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(add(T527, zero(T530), X549), add(T527, zero(X549), T501))\n\nT527 is ground\nT530 is ground\nX549 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: add(T527, zero(T530), X549)\n\nT527 is ground\nT530 is ground\nX549 is free", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: add(T527, zero(T533), T501)\n\nT527 is ground\nT533 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 212 [arrowhead = none ];
212 -> 2;

213 [label="EVAL with clause\ntimes(one(b), X2, X2).\nand substitutionT1 -> one(b),\nT2 -> T5,\nX2 -> T5,\nT3 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 213 [arrowhead = none ];
213 -> 3;

214 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 214 [arrowhead = none ];
214 -> 4;

215 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 215 [arrowhead = none ];
215 -> 5;

216 [label="EVAL with clause\ntimes(zero(X23), X24, zero(X25)) :- times(X23, X24, X25).\nand substitutionX23 -> T14,\nT1 -> zero(T14),\nT2 -> T15,\nX24 -> T15,\nX25 -> T17,\nT3 -> zero(T17),\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 216 [arrowhead = none ];
216 -> 12;

217 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 217 [arrowhead = none ];
217 -> 13;

218 [label="BACKTRACK\nfor clause: times(zero(R), S, zero(RS)) :- times(R, S, RS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 218 [arrowhead = none ];
218 -> 6;

219 [label="ONLY EVAL with clause\ntimes(one(X9), X10, X11) :- ','(times(X9, X10, X12), add(X10, zero(X12), X11)).\nand substitutionX9 -> b,\nT5 -> T8,\nX10 -> T8,\nT3 -> T10,\nX11 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 219 [arrowhead = none ];
219 -> 7;

220 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 220 [arrowhead = none ];
220 -> 8;

221 [label="BACKTRACK\nfor clause: times(one(b), X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 221 [arrowhead = none ];
221 -> 9;

222 [label="BACKTRACK\nfor clause: times(zero(R), S, zero(RS)) :- times(R, S, RS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 222 [arrowhead = none ];
222 -> 10;

223 [label="BACKTRACK\nfor clause: times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 223 [arrowhead = none ];
223 -> 11;

224 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 224 [arrowhead = none ];
224 -> 14;

225 [label="EVAL with clause\ntimes(one(X503), X504, X505) :- ','(times(X503, X504, X506), add(X504, zero(X506), X505)).\nand substitutionX503 -> T498,\nT1 -> one(T498),\nT2 -> T499,\nX504 -> T499,\nT3 -> T501,\nX505 -> T501,\nT500 -> T501", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 225 [arrowhead = none ];
225 -> 193;

226 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 226 [arrowhead = none ];
226 -> 194;

227 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 227 [arrowhead = none ];
227 -> 15;

228 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 228 [arrowhead = none ];
228 -> 16;

229 [label="EVAL with clause\ntimes(one(b), X30, X30).\nand substitutionT14 -> one(b),\nT15 -> T22,\nX30 -> T22,\nT17 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 229 [arrowhead = none ];
229 -> 17;

230 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 230 [arrowhead = none ];
230 -> 18;

231 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 231 [arrowhead = none ];
231 -> 20;

232 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 232 [arrowhead = none ];
232 -> 21;

233 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 233 [arrowhead = none ];
233 -> 19;

234 [label="EVAL with clause\ntimes(zero(X43), X44, zero(X45)) :- times(X43, X44, X45).\nand substitutionX43 -> T35,\nT14 -> zero(T35),\nT15 -> T36,\nX44 -> T36,\nX45 -> T38,\nT17 -> zero(T38),\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 234 [arrowhead = none ];
234 -> 22;

235 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 235 [arrowhead = none ];
235 -> 23;

236 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
21 -> 236 [arrowhead = none ];
236 -> 24;

237 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
21 -> 237 [arrowhead = none ];
237 -> 25;

238 [label="INSTANCE with matching:\nT1 -> T35\nT2 -> T36\nT3 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 238 [arrowhead = none , style=dashed];
238 -> 1[style=dashed];

239 [label="EVAL with clause\ntimes(one(X62), X63, X64) :- ','(times(X62, X63, X65), add(X63, zero(X65), X64)).\nand substitutionX62 -> T53,\nT14 -> one(T53),\nT15 -> T54,\nX63 -> T54,\nT17 -> T56,\nX64 -> T56,\nT55 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 239 [arrowhead = none ];
239 -> 26;

240 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 240 [arrowhead = none ];
240 -> 27;

241 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 241 [arrowhead = none ];
241 -> 191;

242 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
26 -> 242 [arrowhead = none ];
242 -> 28;

243 [label="SPLIT 2\nnew knowledge:\nT53 is ground\nT54 is ground\nT59 is ground\nreplacements:X65 -> T59", fontsize=14, style = filled, fillcolor = violet];
26 -> 243 [arrowhead = none ];
243 -> 29;

244 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
28 -> 244 [arrowhead = none ];
244 -> 30;

245 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
29 -> 245 [arrowhead = none ];
245 -> 44;

246 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 246 [arrowhead = none ];
246 -> 31;

247 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 247 [arrowhead = none ];
247 -> 32;

248 [label="EVAL with clause\ntimes(one(b), X74, X74).\nand substitutionT53 -> one(b),\nT54 -> T66,\nX74 -> T66,\nX65 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 248 [arrowhead = none ];
248 -> 33;

249 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 249 [arrowhead = none ];
249 -> 34;

250 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 250 [arrowhead = none ];
250 -> 36;

251 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 251 [arrowhead = none ];
251 -> 37;

252 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 252 [arrowhead = none ];
252 -> 35;

253 [label="EVAL with clause\ntimes(zero(X91), X92, zero(X93)) :- times(X91, X92, X93).\nand substitutionX91 -> T75,\nT53 -> zero(T75),\nT54 -> T76,\nX92 -> T76,\nX93 -> X94,\nX65 -> zero(X94)", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 253 [arrowhead = none ];
253 -> 38;

254 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 254 [arrowhead = none ];
254 -> 39;

255 [label="EVAL with clause\ntimes(one(X106), X107, X108) :- ','(times(X106, X107, X109), add(X107, zero(X109), X108)).\nand substitutionX106 -> T83,\nT53 -> one(T83),\nT54 -> T84,\nX107 -> T84,\nX65 -> X110,\nX108 -> X110", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 255 [arrowhead = none ];
255 -> 40;

256 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 256 [arrowhead = none ];
256 -> 41;

257 [label="INSTANCE with matching:\nT53 -> T75\nT54 -> T76\nX65 -> X94", fontsize=14, style = filled, fillcolor = lightgrey];
38 -> 257 [arrowhead = none , style=dashed];
257 -> 28[style=dashed];

258 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 258 [arrowhead = none ];
258 -> 42;

259 [label="SPLIT 2\nnew knowledge:\nT83 is ground\nT84 is ground\nT87 is ground\nreplacements:X109 -> T87", fontsize=14, style = filled, fillcolor = violet];
40 -> 259 [arrowhead = none ];
259 -> 43;

260 [label="INSTANCE with matching:\nT53 -> T83\nT54 -> T84\nX65 -> X109", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 260 [arrowhead = none , style=dashed];
260 -> 28[style=dashed];

261 [label="INSTANCE with matching:\nT54 -> T84\nT59 -> T87\nT56 -> X110", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 261 [arrowhead = none , style=dashed];
261 -> 29[style=dashed];

262 [label="BACKTRACK\nfor clause: add(b, b, b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 262 [arrowhead = none ];
262 -> 45;

263 [label="BACKTRACK\nfor clause: add(X, b, X) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 263 [arrowhead = none ];
263 -> 46;

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 264 [arrowhead = none ];
264 -> 47;

265 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 265 [arrowhead = none ];
265 -> 48;

266 [label="EVAL with clause\nadd(b, X120, X120) :- binaryZ(X120).\nand substitutionT54 -> b,\nT59 -> T95,\nX120 -> zero(T95),\nT56 -> zero(T95)", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 266 [arrowhead = none ];
266 -> 49;

267 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 267 [arrowhead = none ];
267 -> 50;

268 [label="ONLY EVAL with clause\nadd(X158, X159, X160) :- addz(X158, X159, X160).\nand substitutionT54 -> T133,\nX158 -> T133,\nT59 -> T134,\nX159 -> zero(T134),\nT56 -> T136,\nX160 -> T136,\nT135 -> T136", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 268 [arrowhead = none ];
268 -> 75;

269 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
49 -> 269 [arrowhead = none ];
269 -> 51;

270 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
51 -> 270 [arrowhead = none ];
270 -> 52;

271 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
51 -> 271 [arrowhead = none ];
271 -> 53;

272 [label="ONLY EVAL with clause\nbinaryZ(zero(X128)) :- binaryZ(X128).\nand substitutionT95 -> T103,\nX128 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 272 [arrowhead = none ];
272 -> 54;

273 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 273 [arrowhead = none ];
273 -> 74;

274 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
54 -> 274 [arrowhead = none ];
274 -> 55;

275 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 275 [arrowhead = none ];
275 -> 56;

276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 276 [arrowhead = none ];
276 -> 57;

277 [label="EVAL with clause\nbinaryZ(zero(X134)) :- binaryZ(X134).\nand substitutionX134 -> T109,\nT103 -> zero(T109)", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 277 [arrowhead = none ];
277 -> 58;

278 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 278 [arrowhead = none ];
278 -> 59;

279 [label="EVAL with clause\nbinaryZ(one(X138)) :- binary(X138).\nand substitutionX138 -> T113,\nT103 -> one(T113)", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 279 [arrowhead = none ];
279 -> 60;

280 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 280 [arrowhead = none ];
280 -> 61;

281 [label="INSTANCE with matching:\nT103 -> T109", fontsize=14, style = filled, fillcolor = lightgrey];
58 -> 281 [arrowhead = none , style=dashed];
281 -> 54[style=dashed];

282 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
60 -> 282 [arrowhead = none ];
282 -> 62;

283 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 283 [arrowhead = none ];
283 -> 63;

284 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 284 [arrowhead = none ];
284 -> 64;

285 [label="EVAL with clause\nbinary(b).\nand substitutionT113 -> b", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 285 [arrowhead = none ];
285 -> 65;

286 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 286 [arrowhead = none ];
286 -> 66;

287 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 287 [arrowhead = none ];
287 -> 68;

288 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 288 [arrowhead = none ];
288 -> 69;

289 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 289 [arrowhead = none ];
289 -> 67;

290 [label="EVAL with clause\nbinary(zero(X143)) :- binaryZ(X143).\nand substitutionX143 -> T118,\nT113 -> zero(T118)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 290 [arrowhead = none ];
290 -> 70;

291 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 291 [arrowhead = none ];
291 -> 71;

292 [label="EVAL with clause\nbinary(one(X147)) :- binary(X147).\nand substitutionX147 -> T122,\nT113 -> one(T122)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 292 [arrowhead = none ];
292 -> 72;

293 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 293 [arrowhead = none ];
293 -> 73;

294 [label="INSTANCE with matching:\nT103 -> T118", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 294 [arrowhead = none , style=dashed];
294 -> 54[style=dashed];

295 [label="INSTANCE with matching:\nT113 -> T122", fontsize=14, style = filled, fillcolor = lightgrey];
72 -> 295 [arrowhead = none , style=dashed];
295 -> 60[style=dashed];

296 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
75 -> 296 [arrowhead = none ];
296 -> 76;

297 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 297 [arrowhead = none ];
297 -> 77;

298 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 298 [arrowhead = none ];
298 -> 78;

299 [label="EVAL with clause\naddz(zero(X176), zero(X177), zero(X178)) :- addz(X176, X177, X178).\nand substitutionX176 -> T152,\nT133 -> zero(T152),\nT134 -> T153,\nX177 -> T153,\nX178 -> T155,\nT136 -> zero(T155),\nT154 -> T155", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 299 [arrowhead = none ];
299 -> 79;

300 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 300 [arrowhead = none ];
300 -> 80;

301 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 301 [arrowhead = none ];
301 -> 185;

302 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
79 -> 302 [arrowhead = none ];
302 -> 81;

303 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
81 -> 303 [arrowhead = none ];
303 -> 82;

304 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
81 -> 304 [arrowhead = none ];
304 -> 83;

305 [label="EVAL with clause\naddz(zero(X194), zero(X195), zero(X196)) :- addz(X194, X195, X196).\nand substitutionX194 -> T171,\nT152 -> zero(T171),\nX195 -> T172,\nT153 -> zero(T172),\nX196 -> T174,\nT155 -> zero(T174),\nT173 -> T174", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 305 [arrowhead = none ];
305 -> 84;

306 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 306 [arrowhead = none ];
306 -> 85;

307 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 307 [arrowhead = none ];
307 -> 86;

308 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 308 [arrowhead = none ];
308 -> 87;

309 [label="INSTANCE with matching:\nT152 -> T171\nT153 -> T172\nT155 -> T174", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 309 [arrowhead = none , style=dashed];
309 -> 79[style=dashed];

310 [label="EVAL with clause\naddz(zero(X212), one(X213), one(X214)) :- addx(X212, X213, X214).\nand substitutionX212 -> T190,\nT152 -> zero(T190),\nX213 -> T191,\nT153 -> one(T191),\nX214 -> T193,\nT155 -> one(T193),\nT192 -> T193", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 310 [arrowhead = none ];
310 -> 88;

311 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 311 [arrowhead = none ];
311 -> 89;

312 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 312 [arrowhead = none ];
312 -> 100;

313 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 313 [arrowhead = none ];
313 -> 101;

314 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
88 -> 314 [arrowhead = none ];
314 -> 90;

315 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
90 -> 315 [arrowhead = none ];
315 -> 91;

316 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
90 -> 316 [arrowhead = none ];
316 -> 92;

317 [label="EVAL with clause\naddx(one(X220), b, one(X220)) :- binary(X220).\nand substitutionX220 -> T199,\nT190 -> one(T199),\nT191 -> b,\nT193 -> one(T199)", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 317 [arrowhead = none ];
317 -> 93;

318 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 318 [arrowhead = none ];
318 -> 94;

319 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
92 -> 319 [arrowhead = none ];
319 -> 95;

320 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
92 -> 320 [arrowhead = none ];
320 -> 96;

321 [label="INSTANCE with matching:\nT113 -> T199", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 321 [arrowhead = none , style=dashed];
321 -> 60[style=dashed];

322 [label="EVAL with clause\naddx(zero(X225), b, zero(X225)) :- binaryZ(X225).\nand substitutionX225 -> T204,\nT190 -> zero(T204),\nT191 -> b,\nT193 -> zero(T204)", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 322 [arrowhead = none ];
322 -> 97;

323 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 323 [arrowhead = none ];
323 -> 98;

324 [label="ONLY EVAL with clause\naddx(X236, X237, X238) :- addz(X236, X237, X238).\nand substitutionT190 -> T216,\nX236 -> T216,\nT191 -> T217,\nX237 -> T217,\nT193 -> T219,\nX238 -> T219,\nT218 -> T219", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 324 [arrowhead = none ];
324 -> 99;

325 [label="INSTANCE with matching:\nT103 -> T204", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 325 [arrowhead = none , style=dashed];
325 -> 54[style=dashed];

326 [label="INSTANCE with matching:\nT152 -> T216\nT153 -> T217\nT155 -> T219", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 326 [arrowhead = none , style=dashed];
326 -> 79[style=dashed];

327 [label="EVAL with clause\naddz(one(X254), zero(X255), one(X256)) :- addy(X254, X255, X256).\nand substitutionX254 -> T235,\nT152 -> one(T235),\nX255 -> T236,\nT153 -> zero(T236),\nX256 -> T238,\nT155 -> one(T238),\nT237 -> T238", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 327 [arrowhead = none ];
327 -> 102;

328 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 328 [arrowhead = none ];
328 -> 103;

329 [label="EVAL with clause\naddz(one(X290), one(X291), zero(X292)) :- addc(X290, X291, X292).\nand substitutionX290 -> T274,\nT152 -> one(T274),\nX291 -> T275,\nT153 -> one(T275),\nX292 -> T277,\nT155 -> zero(T277),\nT276 -> T277", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 329 [arrowhead = none ];
329 -> 114;

330 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 330 [arrowhead = none ];
330 -> 115;

331 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
102 -> 331 [arrowhead = none ];
331 -> 104;

332 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 332 [arrowhead = none ];
332 -> 105;

333 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 333 [arrowhead = none ];
333 -> 106;

334 [label="EVAL with clause\naddy(b, one(X262), one(X262)) :- binary(X262).\nand substitutionT235 -> b,\nX262 -> T244,\nT236 -> one(T244),\nT238 -> one(T244)", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 334 [arrowhead = none ];
334 -> 107;

335 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 335 [arrowhead = none ];
335 -> 108;

336 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
106 -> 336 [arrowhead = none ];
336 -> 109;

337 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
106 -> 337 [arrowhead = none ];
337 -> 110;

338 [label="INSTANCE with matching:\nT113 -> T244", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 338 [arrowhead = none , style=dashed];
338 -> 60[style=dashed];

339 [label="EVAL with clause\naddy(b, zero(X267), zero(X267)) :- binaryZ(X267).\nand substitutionT235 -> b,\nX267 -> T249,\nT236 -> zero(T249),\nT238 -> zero(T249)", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 339 [arrowhead = none ];
339 -> 111;

340 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 340 [arrowhead = none ];
340 -> 112;

341 [label="ONLY EVAL with clause\naddy(X278, X279, X280) :- addz(X278, X279, X280).\nand substitutionT235 -> T261,\nX278 -> T261,\nT236 -> T262,\nX279 -> T262,\nT238 -> T264,\nX280 -> T264,\nT263 -> T264", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 341 [arrowhead = none ];
341 -> 113;

342 [label="INSTANCE with matching:\nT103 -> T249", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 342 [arrowhead = none , style=dashed];
342 -> 54[style=dashed];

343 [label="INSTANCE with matching:\nT152 -> T261\nT153 -> T262\nT155 -> T264", fontsize=14, style = filled, fillcolor = lightgrey];
113 -> 343 [arrowhead = none , style=dashed];
343 -> 79[style=dashed];

344 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
114 -> 344 [arrowhead = none ];
344 -> 116;

345 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
116 -> 345 [arrowhead = none ];
345 -> 117;

346 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
116 -> 346 [arrowhead = none ];
346 -> 118;

347 [label="EVAL with clause\naddc(b, b, one(b)).\nand substitutionT274 -> b,\nT275 -> b,\nT277 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 347 [arrowhead = none ];
347 -> 119;

348 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 348 [arrowhead = none ];
348 -> 120;

349 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
118 -> 349 [arrowhead = none ];
349 -> 122;

350 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
118 -> 350 [arrowhead = none ];
350 -> 123;

351 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 351 [arrowhead = none ];
351 -> 121;

352 [label="EVAL with clause\naddc(X301, b, X302) :- succZ(X301, X302).\nand substitutionT274 -> T286,\nX301 -> T286,\nT275 -> b,\nT277 -> T288,\nX302 -> T288,\nT287 -> T288", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 352 [arrowhead = none ];
352 -> 124;

353 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 353 [arrowhead = none ];
353 -> 125;

354 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 354 [arrowhead = none ];
354 -> 145;

355 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 355 [arrowhead = none ];
355 -> 146;

356 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
124 -> 356 [arrowhead = none ];
356 -> 126;

357 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 357 [arrowhead = none ];
357 -> 127;

358 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 358 [arrowhead = none ];
358 -> 128;

359 [label="EVAL with clause\nsuccZ(zero(X308), one(X308)) :- binaryZ(X308).\nand substitutionX308 -> T294,\nT286 -> zero(T294),\nT288 -> one(T294)", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 359 [arrowhead = none ];
359 -> 129;

360 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 360 [arrowhead = none ];
360 -> 130;

361 [label="EVAL with clause\nsuccZ(one(X314), zero(X315)) :- succ(X314, X315).\nand substitutionX314 -> T300,\nT286 -> one(T300),\nX315 -> T302,\nT288 -> zero(T302),\nT301 -> T302", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 361 [arrowhead = none ];
361 -> 131;

362 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 362 [arrowhead = none ];
362 -> 132;

363 [label="INSTANCE with matching:\nT103 -> T294", fontsize=14, style = filled, fillcolor = lightgrey];
129 -> 363 [arrowhead = none , style=dashed];
363 -> 54[style=dashed];

364 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
131 -> 364 [arrowhead = none ];
364 -> 133;

365 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
133 -> 365 [arrowhead = none ];
365 -> 134;

366 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
133 -> 366 [arrowhead = none ];
366 -> 135;

367 [label="EVAL with clause\nsucc(b, one(b)).\nand substitutionT300 -> b,\nT302 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 367 [arrowhead = none ];
367 -> 136;

368 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 368 [arrowhead = none ];
368 -> 137;

369 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
135 -> 369 [arrowhead = none ];
369 -> 139;

370 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
135 -> 370 [arrowhead = none ];
370 -> 140;

371 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 371 [arrowhead = none ];
371 -> 138;

372 [label="EVAL with clause\nsucc(zero(X320), one(X320)) :- binaryZ(X320).\nand substitutionX320 -> T307,\nT300 -> zero(T307),\nT302 -> one(T307)", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 372 [arrowhead = none ];
372 -> 141;

373 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 373 [arrowhead = none ];
373 -> 142;

374 [label="EVAL with clause\nsucc(one(X326), zero(X327)) :- succ(X326, X327).\nand substitutionX326 -> T313,\nT300 -> one(T313),\nX327 -> T315,\nT302 -> zero(T315),\nT314 -> T315", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 374 [arrowhead = none ];
374 -> 143;

375 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 375 [arrowhead = none ];
375 -> 144;

376 [label="INSTANCE with matching:\nT103 -> T307", fontsize=14, style = filled, fillcolor = lightgrey];
141 -> 376 [arrowhead = none , style=dashed];
376 -> 54[style=dashed];

377 [label="INSTANCE with matching:\nT300 -> T313\nT302 -> T315", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 377 [arrowhead = none , style=dashed];
377 -> 131[style=dashed];

378 [label="EVAL with clause\naddc(b, X336, X337) :- succZ(X336, X337).\nand substitutionT274 -> b,\nT275 -> T324,\nX336 -> T324,\nT277 -> T326,\nX337 -> T326,\nT325 -> T326", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 378 [arrowhead = none ];
378 -> 147;

379 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
145 -> 379 [arrowhead = none ];
379 -> 148;

380 [label="ONLY EVAL with clause\naddc(X348, X349, X350) :- addC(X348, X349, X350).\nand substitutionT274 -> T338,\nX348 -> T338,\nT275 -> T339,\nX349 -> T339,\nT277 -> T341,\nX350 -> T341,\nT340 -> T341", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 380 [arrowhead = none ];
380 -> 149;

381 [label="INSTANCE with matching:\nT286 -> T324\nT288 -> T326", fontsize=14, style = filled, fillcolor = lightgrey];
147 -> 381 [arrowhead = none , style=dashed];
381 -> 124[style=dashed];

382 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
149 -> 382 [arrowhead = none ];
382 -> 150;

383 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
150 -> 383 [arrowhead = none ];
383 -> 151;

384 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
150 -> 384 [arrowhead = none ];
384 -> 152;

385 [label="EVAL with clause\naddC(zero(X366), zero(X367), one(X368)) :- addz(X366, X367, X368).\nand substitutionX366 -> T357,\nT338 -> zero(T357),\nX367 -> T358,\nT339 -> zero(T358),\nX368 -> T360,\nT341 -> one(T360),\nT359 -> T360", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 385 [arrowhead = none ];
385 -> 153;

386 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
151 -> 386 [arrowhead = none ];
386 -> 154;

387 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
152 -> 387 [arrowhead = none ];
387 -> 155;

388 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
152 -> 388 [arrowhead = none ];
388 -> 156;

389 [label="INSTANCE with matching:\nT152 -> T357\nT153 -> T358\nT155 -> T360", fontsize=14, style = filled, fillcolor = lightgrey];
153 -> 389 [arrowhead = none , style=dashed];
389 -> 79[style=dashed];

390 [label="EVAL with clause\naddC(zero(X384), one(X385), zero(X386)) :- addX(X384, X385, X386).\nand substitutionX384 -> T376,\nT338 -> zero(T376),\nX385 -> T377,\nT339 -> one(T377),\nX386 -> T379,\nT341 -> zero(T379),\nT378 -> T379", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 390 [arrowhead = none ];
390 -> 157;

391 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 391 [arrowhead = none ];
391 -> 158;

392 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
156 -> 392 [arrowhead = none ];
392 -> 169;

393 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
156 -> 393 [arrowhead = none ];
393 -> 170;

394 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
157 -> 394 [arrowhead = none ];
394 -> 159;

395 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
159 -> 395 [arrowhead = none ];
395 -> 160;

396 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
159 -> 396 [arrowhead = none ];
396 -> 161;

397 [label="EVAL with clause\naddX(zero(X392), b, one(X392)) :- binaryZ(X392).\nand substitutionX392 -> T385,\nT376 -> zero(T385),\nT377 -> b,\nT379 -> one(T385)", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 397 [arrowhead = none ];
397 -> 162;

398 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 398 [arrowhead = none ];
398 -> 163;

399 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 399 [arrowhead = none ];
399 -> 164;

400 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 400 [arrowhead = none ];
400 -> 165;

401 [label="INSTANCE with matching:\nT103 -> T385", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 401 [arrowhead = none , style=dashed];
401 -> 54[style=dashed];

402 [label="EVAL with clause\naddX(one(X402), b, zero(X403)) :- succ(X402, X403).\nand substitutionX402 -> T395,\nT376 -> one(T395),\nT377 -> b,\nX403 -> T397,\nT379 -> zero(T397),\nT396 -> T397", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 402 [arrowhead = none ];
402 -> 166;

403 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
164 -> 403 [arrowhead = none ];
403 -> 167;

404 [label="ONLY EVAL with clause\naddX(X413, X414, X415) :- addC(X413, X414, X415).\nand substitutionT376 -> T408,\nX413 -> T408,\nT377 -> T409,\nX414 -> T409,\nT379 -> T411,\nX415 -> T411,\nT410 -> T411", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 404 [arrowhead = none ];
404 -> 168;

405 [label="INSTANCE with matching:\nT300 -> T395\nT302 -> T397", fontsize=14, style = filled, fillcolor = lightgrey];
166 -> 405 [arrowhead = none , style=dashed];
405 -> 131[style=dashed];

406 [label="INSTANCE with matching:\nT338 -> T408\nT339 -> T409\nT341 -> T411", fontsize=14, style = filled, fillcolor = lightgrey];
168 -> 406 [arrowhead = none , style=dashed];
406 -> 149[style=dashed];

407 [label="EVAL with clause\naddC(one(X431), zero(X432), zero(X433)) :- addY(X431, X432, X433).\nand substitutionX431 -> T427,\nT338 -> one(T427),\nX432 -> T428,\nT339 -> zero(T428),\nX433 -> T430,\nT341 -> zero(T430),\nT429 -> T430", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 407 [arrowhead = none ];
407 -> 171;

408 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
169 -> 408 [arrowhead = none ];
408 -> 172;

409 [label="EVAL with clause\naddC(one(X472), one(X473), one(X474)) :- addc(X472, X473, X474).\nand substitutionX472 -> T472,\nT338 -> one(T472),\nX473 -> T473,\nT339 -> one(T473),\nX474 -> T475,\nT341 -> one(T475),\nT474 -> T475", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 409 [arrowhead = none ];
409 -> 183;

410 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
170 -> 410 [arrowhead = none ];
410 -> 184;

411 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
171 -> 411 [arrowhead = none ];
411 -> 173;

412 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
173 -> 412 [arrowhead = none ];
412 -> 174;

413 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
173 -> 413 [arrowhead = none ];
413 -> 175;

414 [label="EVAL with clause\naddY(b, zero(X439), one(X439)) :- binaryZ(X439).\nand substitutionT427 -> b,\nX439 -> T436,\nT428 -> zero(T436),\nT430 -> one(T436)", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 414 [arrowhead = none ];
414 -> 176;

415 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
174 -> 415 [arrowhead = none ];
415 -> 177;

416 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
175 -> 416 [arrowhead = none ];
416 -> 178;

417 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
175 -> 417 [arrowhead = none ];
417 -> 179;

418 [label="INSTANCE with matching:\nT103 -> T436", fontsize=14, style = filled, fillcolor = lightgrey];
176 -> 418 [arrowhead = none , style=dashed];
418 -> 54[style=dashed];

419 [label="EVAL with clause\naddY(b, one(X449), zero(X450)) :- succ(X449, X450).\nand substitutionT427 -> b,\nX449 -> T446,\nT428 -> one(T446),\nX450 -> T448,\nT430 -> zero(T448),\nT447 -> T448", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 419 [arrowhead = none ];
419 -> 180;

420 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
178 -> 420 [arrowhead = none ];
420 -> 181;

421 [label="ONLY EVAL with clause\naddY(X460, X461, X462) :- addC(X460, X461, X462).\nand substitutionT427 -> T459,\nX460 -> T459,\nT428 -> T460,\nX461 -> T460,\nT430 -> T462,\nX462 -> T462,\nT461 -> T462", fontsize=14, style = filled, fillcolor = lightblue];
179 -> 421 [arrowhead = none ];
421 -> 182;

422 [label="INSTANCE with matching:\nT300 -> T446\nT302 -> T448", fontsize=14, style = filled, fillcolor = lightgrey];
180 -> 422 [arrowhead = none , style=dashed];
422 -> 131[style=dashed];

423 [label="INSTANCE with matching:\nT338 -> T459\nT339 -> T460\nT341 -> T462", fontsize=14, style = filled, fillcolor = lightgrey];
182 -> 423 [arrowhead = none , style=dashed];
423 -> 149[style=dashed];

424 [label="INSTANCE with matching:\nT274 -> T472\nT275 -> T473\nT277 -> T475", fontsize=14, style = filled, fillcolor = lightgrey];
183 -> 424 [arrowhead = none , style=dashed];
424 -> 114[style=dashed];

425 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
185 -> 425 [arrowhead = none ];
425 -> 186;

426 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
185 -> 426 [arrowhead = none ];
426 -> 187;

427 [label="EVAL with clause\naddz(one(X490), zero(X491), one(X492)) :- addy(X490, X491, X492).\nand substitutionX490 -> T489,\nT133 -> one(T489),\nT134 -> T490,\nX491 -> T490,\nX492 -> T492,\nT136 -> one(T492),\nT491 -> T492", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 427 [arrowhead = none ];
427 -> 188;

428 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
186 -> 428 [arrowhead = none ];
428 -> 189;

429 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
187 -> 429 [arrowhead = none ];
429 -> 190;

430 [label="INSTANCE with matching:\nT235 -> T489\nT236 -> T490\nT238 -> T492", fontsize=14, style = filled, fillcolor = lightgrey];
188 -> 430 [arrowhead = none , style=dashed];
430 -> 102[style=dashed];

431 [label="BACKTRACK\nfor clause: times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
191 -> 431 [arrowhead = none ];
431 -> 192;

432 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
193 -> 432 [arrowhead = none ];
432 -> 195;

433 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 433 [arrowhead = none ];
433 -> 196;

434 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 434 [arrowhead = none ];
434 -> 197;

435 [label="EVAL with clause\ntimes(one(b), X511, X511).\nand substitutionT498 -> one(b),\nT499 -> T506,\nX511 -> T506,\nX506 -> T506", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 435 [arrowhead = none ];
435 -> 198;

436 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 436 [arrowhead = none ];
436 -> 199;

437 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
197 -> 437 [arrowhead = none ];
437 -> 200;

438 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
197 -> 438 [arrowhead = none ];
438 -> 201;

439 [label="INSTANCE with matching:\nT54 -> T506\nT59 -> T506\nT56 -> T501", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 439 [arrowhead = none , style=dashed];
439 -> 29[style=dashed];

440 [label="EVAL with clause\ntimes(zero(X528), X529, zero(X530)) :- times(X528, X529, X530).\nand substitutionX528 -> T515,\nT498 -> zero(T515),\nT499 -> T516,\nX529 -> T516,\nX530 -> X531,\nX506 -> zero(X531)", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 440 [arrowhead = none ];
440 -> 202;

441 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 441 [arrowhead = none ];
441 -> 203;

442 [label="EVAL with clause\ntimes(one(X545), X546, X547) :- ','(times(X545, X546, X548), add(X546, zero(X548), X547)).\nand substitutionX545 -> T526,\nT498 -> one(T526),\nT499 -> T527,\nX546 -> T527,\nX506 -> X549,\nX547 -> X549", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 442 [arrowhead = none ];
442 -> 206;

443 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 443 [arrowhead = none ];
443 -> 207;

444 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
202 -> 444 [arrowhead = none ];
444 -> 204;

445 [label="SPLIT 2\nnew knowledge:\nT515 is ground\nT516 is ground\nT519 is ground\nreplacements:X531 -> T519", fontsize=14, style = filled, fillcolor = violet];
202 -> 445 [arrowhead = none ];
445 -> 205;

446 [label="INSTANCE with matching:\nT53 -> T515\nT54 -> T516\nX65 -> X531", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 446 [arrowhead = none , style=dashed];
446 -> 28[style=dashed];

447 [label="INSTANCE with matching:\nT54 -> T516\nT59 -> zero(T519)\nT56 -> T501", fontsize=14, style = filled, fillcolor = lightgrey];
205 -> 447 [arrowhead = none , style=dashed];
447 -> 29[style=dashed];

448 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
206 -> 448 [arrowhead = none ];
448 -> 208;

449 [label="SPLIT 2\nnew knowledge:\nT526 is ground\nT527 is ground\nT530 is ground\nreplacements:X548 -> T530", fontsize=14, style = filled, fillcolor = violet];
206 -> 449 [arrowhead = none ];
449 -> 209;

450 [label="INSTANCE with matching:\nT53 -> T526\nT54 -> T527\nX65 -> X548", fontsize=14, style = filled, fillcolor = lightgrey];
208 -> 450 [arrowhead = none , style=dashed];
450 -> 28[style=dashed];

451 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
209 -> 451 [arrowhead = none ];
451 -> 210;

452 [label="SPLIT 2\nnew knowledge:\nT527 is ground\nT530 is ground\nT533 is ground\nreplacements:X549 -> T533", fontsize=14, style = filled, fillcolor = violet];
209 -> 452 [arrowhead = none ];
452 -> 211;

453 [label="INSTANCE with matching:\nT54 -> T527\nT59 -> T530\nT56 -> X549", fontsize=14, style = filled, fillcolor = lightgrey];
210 -> 453 [arrowhead = none , style=dashed];
453 -> 29[style=dashed];

454 [label="INSTANCE with matching:\nT54 -> T527\nT59 -> T533\nT56 -> T501", fontsize=14, style = filled, fillcolor = lightgrey];
211 -> 454 [arrowhead = none , style=dashed];
454 -> 29[style=dashed];

}

(2) Obligation:

Triples:

timesC(zero(X1), X2, zero(X3)) :- timesC(X1, X2, X3).
timesC(one(X1), X2, X3) :- timesC(X1, X2, X4).
timesC(one(X1), X2, X3) :- ','(timescC(X1, X2, X4), addB(X2, X4, X3)).
addB(b, X1, zero(X1)) :- binaryZD(X1).
addB(zero(X1), X2, zero(X3)) :- addzE(X1, X2, X3).
addB(one(X1), X2, one(X3)) :- addyF(X1, X2, X3).
binaryZD(zero(X1)) :- binaryZD(X1).
binaryZD(one(X1)) :- binaryG(X1).
binaryG(zero(X1)) :- binaryZD(X1).
binaryG(one(X1)) :- binaryG(X1).
addzE(zero(X1), zero(X2), zero(X3)) :- addzE(X1, X2, X3).
addzE(zero(one(X1)), one(b), one(one(X1))) :- binaryG(X1).
addzE(zero(zero(X1)), one(b), one(zero(X1))) :- binaryZD(X1).
addzE(zero(X1), one(X2), one(X3)) :- addzE(X1, X2, X3).
addzE(one(X1), zero(X2), one(X3)) :- addyF(X1, X2, X3).
addzE(one(X1), one(X2), zero(X3)) :- addcH(X1, X2, X3).
succI(zero(X1), one(X1)) :- binaryZD(X1).
succI(one(X1), zero(X2)) :- succI(X1, X2).
succZJ(zero(X1), one(X1)) :- binaryZD(X1).
succZJ(one(X1), zero(X2)) :- succI(X1, X2).
addCK(zero(X1), zero(X2), one(X3)) :- addzE(X1, X2, X3).
addCK(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZD(X1).
addCK(zero(one(X1)), one(b), zero(zero(X2))) :- succI(X1, X2).
addCK(zero(X1), one(X2), zero(X3)) :- addCK(X1, X2, X3).
addCK(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZD(X1).
addCK(one(b), zero(one(X1)), zero(zero(X2))) :- succI(X1, X2).
addCK(one(X1), zero(X2), zero(X3)) :- addCK(X1, X2, X3).
addCK(one(X1), one(X2), one(X3)) :- addcH(X1, X2, X3).
addcH(X1, b, X2) :- succZJ(X1, X2).
addcH(b, X1, X2) :- succZJ(X1, X2).
addcH(X1, X2, X3) :- addCK(X1, X2, X3).
addyF(b, one(X1), one(X1)) :- binaryG(X1).
addyF(b, zero(X1), zero(X1)) :- binaryZD(X1).
addyF(X1, X2, X3) :- addzE(X1, X2, X3).
timesA(zero(zero(X1)), X2, zero(zero(X3))) :- timesA(X1, X2, X3).
timesA(zero(one(X1)), X2, zero(X3)) :- timesC(X1, X2, X4).
timesA(zero(one(X1)), X2, zero(X3)) :- ','(timescC(X1, X2, X4), addB(X2, X4, X3)).
timesA(one(one(b)), X1, X2) :- addB(X1, X1, X2).
timesA(one(zero(X1)), X2, X3) :- timesC(X1, X2, X4).
timesA(one(zero(X1)), X2, X3) :- ','(timescC(X1, X2, X4), addB(X2, zero(X4), X3)).
timesA(one(one(X1)), X2, X3) :- timesC(X1, X2, X4).
timesA(one(one(X1)), X2, X3) :- ','(timescC(X1, X2, X4), addB(X2, X4, X5)).
timesA(one(one(X1)), X2, X3) :- ','(timescC(X1, X2, X4), ','(addcB(X2, X4, X5), addB(X2, X5, X3))).

Clauses:

timescA(one(b), X1, X1).
timescA(zero(one(b)), X1, zero(X1)).
timescA(zero(zero(X1)), X2, zero(zero(X3))) :- timescA(X1, X2, X3).
timescA(zero(one(X1)), X2, zero(X3)) :- ','(timescC(X1, X2, X4), addcB(X2, X4, X3)).
timescA(one(one(b)), X1, X2) :- addcB(X1, X1, X2).
timescA(one(zero(X1)), X2, X3) :- ','(timescC(X1, X2, X4), addcB(X2, zero(X4), X3)).
timescA(one(one(X1)), X2, X3) :- ','(timescC(X1, X2, X4), ','(addcB(X2, X4, X5), addcB(X2, X5, X3))).
timescC(one(b), X1, X1).
timescC(zero(X1), X2, zero(X3)) :- timescC(X1, X2, X3).
timescC(one(X1), X2, X3) :- ','(timescC(X1, X2, X4), addcB(X2, X4, X3)).
addcB(b, X1, zero(X1)) :- binaryZcD(X1).
addcB(zero(X1), X2, zero(X3)) :- addzcE(X1, X2, X3).
addcB(one(X1), X2, one(X3)) :- addycF(X1, X2, X3).
binaryZcD(zero(X1)) :- binaryZcD(X1).
binaryZcD(one(X1)) :- binarycG(X1).
binarycG(b).
binarycG(zero(X1)) :- binaryZcD(X1).
binarycG(one(X1)) :- binarycG(X1).
addzcE(zero(X1), zero(X2), zero(X3)) :- addzcE(X1, X2, X3).
addzcE(zero(one(X1)), one(b), one(one(X1))) :- binarycG(X1).
addzcE(zero(zero(X1)), one(b), one(zero(X1))) :- binaryZcD(X1).
addzcE(zero(X1), one(X2), one(X3)) :- addzcE(X1, X2, X3).
addzcE(one(X1), zero(X2), one(X3)) :- addycF(X1, X2, X3).
addzcE(one(X1), one(X2), zero(X3)) :- addccH(X1, X2, X3).
succcI(b, one(b)).
succcI(zero(X1), one(X1)) :- binaryZcD(X1).
succcI(one(X1), zero(X2)) :- succcI(X1, X2).
succZcJ(zero(X1), one(X1)) :- binaryZcD(X1).
succZcJ(one(X1), zero(X2)) :- succcI(X1, X2).
addCcK(zero(X1), zero(X2), one(X3)) :- addzcE(X1, X2, X3).
addCcK(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZcD(X1).
addCcK(zero(one(X1)), one(b), zero(zero(X2))) :- succcI(X1, X2).
addCcK(zero(X1), one(X2), zero(X3)) :- addCcK(X1, X2, X3).
addCcK(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZcD(X1).
addCcK(one(b), zero(one(X1)), zero(zero(X2))) :- succcI(X1, X2).
addCcK(one(X1), zero(X2), zero(X3)) :- addCcK(X1, X2, X3).
addCcK(one(X1), one(X2), one(X3)) :- addccH(X1, X2, X3).
addccH(b, b, one(b)).
addccH(X1, b, X2) :- succZcJ(X1, X2).
addccH(b, X1, X2) :- succZcJ(X1, X2).
addccH(X1, X2, X3) :- addCcK(X1, X2, X3).
addycF(b, one(X1), one(X1)) :- binarycG(X1).
addycF(b, zero(X1), zero(X1)) :- binaryZcD(X1).
addycF(X1, X2, X3) :- addzcE(X1, X2, X3).

Afs:

timesA(x1, x2, x3) = timesA(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
timesA_in: (b,b,f)
timesC_in: (b,b,f)
timescC_in: (b,b,f)
addcB_in: (b,b,f)
binaryZcD_in: (b)
binarycG_in: (b)
addzcE_in: (b,b,f)
addycF_in: (b,b,f)
addccH_in: (b,b,f)
succZcJ_in: (b,f)
succcI_in: (b,f)
addCcK_in: (b,b,f)
addB_in: (b,b,f)
binaryZD_in: (b)
binaryG_in: (b)
addzE_in: (b,b,f)
addyF_in: (b,b,f)
addcH_in: (b,b,f)
succZJ_in: (b,f)
succI_in: (b,f)
addCK_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

TIMESA_IN_GGA(zero(zero(X1)), X2, zero(zero(X3))) → U36_GGA(X1, X2, X3, timesA_in_gga(X1, X2, X3))
TIMESA_IN_GGA(zero(zero(X1)), X2, zero(zero(X3))) → TIMESA_IN_GGA(X1, X2, X3)
TIMESA_IN_GGA(zero(one(X1)), X2, zero(X3)) → U37_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X4))
TIMESA_IN_GGA(zero(one(X1)), X2, zero(X3)) → TIMESC_IN_GGA(X1, X2, X4)
TIMESC_IN_GGA(zero(X1), X2, zero(X3)) → U1_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X3))
TIMESC_IN_GGA(zero(X1), X2, zero(X3)) → TIMESC_IN_GGA(X1, X2, X3)
TIMESC_IN_GGA(one(X1), X2, X3) → U2_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X4))
TIMESC_IN_GGA(one(X1), X2, X3) → TIMESC_IN_GGA(X1, X2, X4)
TIMESC_IN_GGA(one(X1), X2, X3) → U3_GGA(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U3_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U4_GGA(X1, X2, X3, addB_in_gga(X2, X4, X3))
U3_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → ADDB_IN_GGA(X2, X4, X3)
ADDB_IN_GGA(b, X1, zero(X1)) → U5_GGA(X1, binaryZD_in_g(X1))
ADDB_IN_GGA(b, X1, zero(X1)) → BINARYZD_IN_G(X1)
BINARYZD_IN_G(zero(X1)) → U8_G(X1, binaryZD_in_g(X1))
BINARYZD_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYZD_IN_G(one(X1)) → U9_G(X1, binaryG_in_g(X1))
BINARYZD_IN_G(one(X1)) → BINARYG_IN_G(X1)
BINARYG_IN_G(zero(X1)) → U10_G(X1, binaryZD_in_g(X1))
BINARYG_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYG_IN_G(one(X1)) → U11_G(X1, binaryG_in_g(X1))
BINARYG_IN_G(one(X1)) → BINARYG_IN_G(X1)
ADDB_IN_GGA(zero(X1), X2, zero(X3)) → U6_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDB_IN_GGA(zero(X1), X2, zero(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(zero(X1), zero(X2), zero(X3)) → U12_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDZE_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(zero(one(X1)), one(b), one(one(X1))) → U13_GGA(X1, binaryG_in_g(X1))
ADDZE_IN_GGA(zero(one(X1)), one(b), one(one(X1))) → BINARYG_IN_G(X1)
ADDZE_IN_GGA(zero(zero(X1)), one(b), one(zero(X1))) → U14_GGA(X1, binaryZD_in_g(X1))
ADDZE_IN_GGA(zero(zero(X1)), one(b), one(zero(X1))) → BINARYZD_IN_G(X1)
ADDZE_IN_GGA(zero(X1), one(X2), one(X3)) → U15_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDZE_IN_GGA(zero(X1), one(X2), one(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(one(X1), zero(X2), one(X3)) → U16_GGA(X1, X2, X3, addyF_in_gga(X1, X2, X3))
ADDZE_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYF_IN_GGA(X1, X2, X3)
ADDYF_IN_GGA(b, one(X1), one(X1)) → U33_GGA(X1, binaryG_in_g(X1))
ADDYF_IN_GGA(b, one(X1), one(X1)) → BINARYG_IN_G(X1)
ADDYF_IN_GGA(b, zero(X1), zero(X1)) → U34_GGA(X1, binaryZD_in_g(X1))
ADDYF_IN_GGA(b, zero(X1), zero(X1)) → BINARYZD_IN_G(X1)
ADDYF_IN_GGA(X1, X2, X3) → U35_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDYF_IN_GGA(X1, X2, X3) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(one(X1), one(X2), zero(X3)) → U17_GGA(X1, X2, X3, addcH_in_gga(X1, X2, X3))
ADDZE_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCH_IN_GGA(X1, X2, X3)
ADDCH_IN_GGA(X1, b, X2) → U30_GGA(X1, X2, succZJ_in_ga(X1, X2))
ADDCH_IN_GGA(X1, b, X2) → SUCCZJ_IN_GA(X1, X2)
SUCCZJ_IN_GA(zero(X1), one(X1)) → U20_GA(X1, binaryZD_in_g(X1))
SUCCZJ_IN_GA(zero(X1), one(X1)) → BINARYZD_IN_G(X1)
SUCCZJ_IN_GA(one(X1), zero(X2)) → U21_GA(X1, X2, succI_in_ga(X1, X2))
SUCCZJ_IN_GA(one(X1), zero(X2)) → SUCCI_IN_GA(X1, X2)
SUCCI_IN_GA(zero(X1), one(X1)) → U18_GA(X1, binaryZD_in_g(X1))
SUCCI_IN_GA(zero(X1), one(X1)) → BINARYZD_IN_G(X1)
SUCCI_IN_GA(one(X1), zero(X2)) → U19_GA(X1, X2, succI_in_ga(X1, X2))
SUCCI_IN_GA(one(X1), zero(X2)) → SUCCI_IN_GA(X1, X2)
ADDCH_IN_GGA(b, X1, X2) → U31_GGA(X1, X2, succZJ_in_ga(X1, X2))
ADDCH_IN_GGA(b, X1, X2) → SUCCZJ_IN_GA(X1, X2)
ADDCH_IN_GGA(X1, X2, X3) → U32_GGA(X1, X2, X3, addCK_in_gga(X1, X2, X3))
ADDCH_IN_GGA(X1, X2, X3) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(zero(X1), zero(X2), one(X3)) → U22_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDCK_IN_GGA(zero(X1), zero(X2), one(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(zero(zero(X1)), one(b), zero(one(X1))) → U23_GGA(X1, binaryZD_in_g(X1))
ADDCK_IN_GGA(zero(zero(X1)), one(b), zero(one(X1))) → BINARYZD_IN_G(X1)
ADDCK_IN_GGA(zero(one(X1)), one(b), zero(zero(X2))) → U24_GGA(X1, X2, succI_in_ga(X1, X2))
ADDCK_IN_GGA(zero(one(X1)), one(b), zero(zero(X2))) → SUCCI_IN_GA(X1, X2)
ADDCK_IN_GGA(zero(X1), one(X2), zero(X3)) → U25_GGA(X1, X2, X3, addCK_in_gga(X1, X2, X3))
ADDCK_IN_GGA(zero(X1), one(X2), zero(X3)) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(one(b), zero(zero(X1)), zero(one(X1))) → U26_GGA(X1, binaryZD_in_g(X1))
ADDCK_IN_GGA(one(b), zero(zero(X1)), zero(one(X1))) → BINARYZD_IN_G(X1)
ADDCK_IN_GGA(one(b), zero(one(X1)), zero(zero(X2))) → U27_GGA(X1, X2, succI_in_ga(X1, X2))
ADDCK_IN_GGA(one(b), zero(one(X1)), zero(zero(X2))) → SUCCI_IN_GA(X1, X2)
ADDCK_IN_GGA(one(X1), zero(X2), zero(X3)) → U28_GGA(X1, X2, X3, addCK_in_gga(X1, X2, X3))
ADDCK_IN_GGA(one(X1), zero(X2), zero(X3)) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(one(X1), one(X2), one(X3)) → U29_GGA(X1, X2, X3, addcH_in_gga(X1, X2, X3))
ADDCK_IN_GGA(one(X1), one(X2), one(X3)) → ADDCH_IN_GGA(X1, X2, X3)
ADDB_IN_GGA(one(X1), X2, one(X3)) → U7_GGA(X1, X2, X3, addyF_in_gga(X1, X2, X3))
ADDB_IN_GGA(one(X1), X2, one(X3)) → ADDYF_IN_GGA(X1, X2, X3)
TIMESA_IN_GGA(zero(one(X1)), X2, zero(X3)) → U38_GGA(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U38_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U39_GGA(X1, X2, X3, addB_in_gga(X2, X4, X3))
U38_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → ADDB_IN_GGA(X2, X4, X3)
TIMESA_IN_GGA(one(one(b)), X1, X2) → U40_GGA(X1, X2, addB_in_gga(X1, X1, X2))
TIMESA_IN_GGA(one(one(b)), X1, X2) → ADDB_IN_GGA(X1, X1, X2)
TIMESA_IN_GGA(one(zero(X1)), X2, X3) → U41_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X4))
TIMESA_IN_GGA(one(zero(X1)), X2, X3) → TIMESC_IN_GGA(X1, X2, X4)
TIMESA_IN_GGA(one(zero(X1)), X2, X3) → U42_GGA(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U42_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U43_GGA(X1, X2, X3, addB_in_gga(X2, zero(X4), X3))
U42_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → ADDB_IN_GGA(X2, zero(X4), X3)
TIMESA_IN_GGA(one(one(X1)), X2, X3) → U44_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X4))
TIMESA_IN_GGA(one(one(X1)), X2, X3) → TIMESC_IN_GGA(X1, X2, X4)
TIMESA_IN_GGA(one(one(X1)), X2, X3) → U45_GGA(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U45_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U46_GGA(X1, X2, X3, addB_in_gga(X2, X4, X5))
U45_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → ADDB_IN_GGA(X2, X4, X5)
U45_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U47_GGA(X1, X2, X3, addcB_in_gga(X2, X4, X5))
U47_GGA(X1, X2, X3, addcB_out_gga(X2, X4, X5)) → U48_GGA(X1, X2, X3, addB_in_gga(X2, X5, X3))
U47_GGA(X1, X2, X3, addcB_out_gga(X2, X4, X5)) → ADDB_IN_GGA(X2, X5, X3)

The TRS R consists of the following rules:

timescC_in_gga(one(b), X1, X1) → timescC_out_gga(one(b), X1, X1)
timescC_in_gga(zero(X1), X2, zero(X3)) → U59_gga(X1, X2, X3, timescC_in_gga(X1, X2, X3))
timescC_in_gga(one(X1), X2, X3) → U60_gga(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U60_gga(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U61_gga(X1, X2, X3, addcB_in_gga(X2, X4, X3))
addcB_in_gga(b, X1, zero(X1)) → U62_gga(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(zero(X1)) → U65_g(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(one(X1)) → U66_g(X1, binarycG_in_g(X1))
binarycG_in_g(b) → binarycG_out_g(b)
binarycG_in_g(zero(X1)) → U67_g(X1, binaryZcD_in_g(X1))
U67_g(X1, binaryZcD_out_g(X1)) → binarycG_out_g(zero(X1))
binarycG_in_g(one(X1)) → U68_g(X1, binarycG_in_g(X1))
U68_g(X1, binarycG_out_g(X1)) → binarycG_out_g(one(X1))
U66_g(X1, binarycG_out_g(X1)) → binaryZcD_out_g(one(X1))
U65_g(X1, binaryZcD_out_g(X1)) → binaryZcD_out_g(zero(X1))
U62_gga(X1, binaryZcD_out_g(X1)) → addcB_out_gga(b, X1, zero(X1))
addcB_in_gga(zero(X1), X2, zero(X3)) → U63_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(X1), zero(X2), zero(X3)) → U69_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(one(X1)), one(b), one(one(X1))) → U70_gga(X1, binarycG_in_g(X1))
U70_gga(X1, binarycG_out_g(X1)) → addzcE_out_gga(zero(one(X1)), one(b), one(one(X1)))
addzcE_in_gga(zero(zero(X1)), one(b), one(zero(X1))) → U71_gga(X1, binaryZcD_in_g(X1))
U71_gga(X1, binaryZcD_out_g(X1)) → addzcE_out_gga(zero(zero(X1)), one(b), one(zero(X1)))
addzcE_in_gga(zero(X1), one(X2), one(X3)) → U72_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), zero(X2), one(X3)) → U73_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
addycF_in_gga(b, one(X1), one(X1)) → U90_gga(X1, binarycG_in_g(X1))
U90_gga(X1, binarycG_out_g(X1)) → addycF_out_gga(b, one(X1), one(X1))
addycF_in_gga(b, zero(X1), zero(X1)) → U91_gga(X1, binaryZcD_in_g(X1))
U91_gga(X1, binaryZcD_out_g(X1)) → addycF_out_gga(b, zero(X1), zero(X1))
addycF_in_gga(X1, X2, X3) → U92_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), one(X2), zero(X3)) → U74_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
addccH_in_gga(b, b, one(b)) → addccH_out_gga(b, b, one(b))
addccH_in_gga(X1, b, X2) → U87_gga(X1, X2, succZcJ_in_ga(X1, X2))
succZcJ_in_ga(zero(X1), one(X1)) → U77_ga(X1, binaryZcD_in_g(X1))
U77_ga(X1, binaryZcD_out_g(X1)) → succZcJ_out_ga(zero(X1), one(X1))
succZcJ_in_ga(one(X1), zero(X2)) → U78_ga(X1, X2, succcI_in_ga(X1, X2))
succcI_in_ga(b, one(b)) → succcI_out_ga(b, one(b))
succcI_in_ga(zero(X1), one(X1)) → U75_ga(X1, binaryZcD_in_g(X1))
U75_ga(X1, binaryZcD_out_g(X1)) → succcI_out_ga(zero(X1), one(X1))
succcI_in_ga(one(X1), zero(X2)) → U76_ga(X1, X2, succcI_in_ga(X1, X2))
U76_ga(X1, X2, succcI_out_ga(X1, X2)) → succcI_out_ga(one(X1), zero(X2))
U78_ga(X1, X2, succcI_out_ga(X1, X2)) → succZcJ_out_ga(one(X1), zero(X2))
U87_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(X1, b, X2)
addccH_in_gga(b, X1, X2) → U88_gga(X1, X2, succZcJ_in_ga(X1, X2))
U88_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(b, X1, X2)
addccH_in_gga(X1, X2, X3) → U89_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(zero(X1), zero(X2), one(X3)) → U79_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
U79_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), zero(X2), one(X3))
addCcK_in_gga(zero(zero(X1)), one(b), zero(one(X1))) → U80_gga(X1, binaryZcD_in_g(X1))
U80_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(zero(zero(X1)), one(b), zero(one(X1)))
addCcK_in_gga(zero(one(X1)), one(b), zero(zero(X2))) → U81_gga(X1, X2, succcI_in_ga(X1, X2))
U81_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(zero(one(X1)), one(b), zero(zero(X2)))
addCcK_in_gga(zero(X1), one(X2), zero(X3)) → U82_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(b), zero(zero(X1)), zero(one(X1))) → U83_gga(X1, binaryZcD_in_g(X1))
U83_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(one(b), zero(zero(X1)), zero(one(X1)))
addCcK_in_gga(one(b), zero(one(X1)), zero(zero(X2))) → U84_gga(X1, X2, succcI_in_ga(X1, X2))
U84_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(one(b), zero(one(X1)), zero(zero(X2)))
addCcK_in_gga(one(X1), zero(X2), zero(X3)) → U85_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(X1), one(X2), one(X3)) → U86_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
U86_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), one(X2), one(X3))
U85_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), zero(X2), zero(X3))
U82_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), one(X2), zero(X3))
U89_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addccH_out_gga(X1, X2, X3)
U74_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), one(X2), zero(X3))
U92_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addycF_out_gga(X1, X2, X3)
U73_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), zero(X2), one(X3))
U72_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), one(X2), one(X3))
U69_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), zero(X2), zero(X3))
U63_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addcB_out_gga(zero(X1), X2, zero(X3))
addcB_in_gga(one(X1), X2, one(X3)) → U64_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
U64_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addcB_out_gga(one(X1), X2, one(X3))
U61_gga(X1, X2, X3, addcB_out_gga(X2, X4, X3)) → timescC_out_gga(one(X1), X2, X3)
U59_gga(X1, X2, X3, timescC_out_gga(X1, X2, X3)) → timescC_out_gga(zero(X1), X2, zero(X3))

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3) = timesA_in_gga(x1, x2)
zero(x1) = zero(x1)
one(x1) = one(x1)
timesC_in_gga(x1, x2, x3) = timesC_in_gga(x1, x2)
timescC_in_gga(x1, x2, x3) = timescC_in_gga(x1, x2)
b = b
timescC_out_gga(x1, x2, x3) = timescC_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addcB_in_gga(x1, x2, x3) = addcB_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZcD_in_g(x1) = binaryZcD_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binarycG_in_g(x1) = binarycG_in_g(x1)
binarycG_out_g(x1) = binarycG_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZcD_out_g(x1) = binaryZcD_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addcB_out_gga(x1, x2, x3) = addcB_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzcE_in_gga(x1, x2, x3) = addzcE_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzcE_out_gga(x1, x2, x3) = addzcE_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addycF_in_gga(x1, x2, x3) = addycF_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addycF_out_gga(x1, x2, x3) = addycF_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addccH_in_gga(x1, x2, x3) = addccH_in_gga(x1, x2)
addccH_out_gga(x1, x2, x3) = addccH_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZcJ_in_ga(x1, x2) = succZcJ_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZcJ_out_ga(x1, x2) = succZcJ_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succcI_in_ga(x1, x2) = succcI_in_ga(x1)
succcI_out_ga(x1, x2) = succcI_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCcK_in_gga(x1, x2, x3) = addCcK_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCcK_out_gga(x1, x2, x3) = addCcK_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
addB_in_gga(x1, x2, x3) = addB_in_gga(x1, x2)
binaryZD_in_g(x1) = binaryZD_in_g(x1)
binaryG_in_g(x1) = binaryG_in_g(x1)
addzE_in_gga(x1, x2, x3) = addzE_in_gga(x1, x2)
addyF_in_gga(x1, x2, x3) = addyF_in_gga(x1, x2)
addcH_in_gga(x1, x2, x3) = addcH_in_gga(x1, x2)
succZJ_in_ga(x1, x2) = succZJ_in_ga(x1)
succI_in_ga(x1, x2) = succI_in_ga(x1)
addCK_in_gga(x1, x2, x3) = addCK_in_gga(x1, x2)
TIMESA_IN_GGA(x1, x2, x3) = TIMESA_IN_GGA(x1, x2)
U36_GGA(x1, x2, x3, x4) = U36_GGA(x1, x2, x4)
U37_GGA(x1, x2, x3, x4) = U37_GGA(x1, x2, x4)
TIMESC_IN_GGA(x1, x2, x3) = TIMESC_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4) = U4_GGA(x1, x2, x4)
ADDB_IN_GGA(x1, x2, x3) = ADDB_IN_GGA(x1, x2)
U5_GGA(x1, x2) = U5_GGA(x1, x2)
BINARYZD_IN_G(x1) = BINARYZD_IN_G(x1)
U8_G(x1, x2) = U8_G(x1, x2)
U9_G(x1, x2) = U9_G(x1, x2)
BINARYG_IN_G(x1) = BINARYG_IN_G(x1)
U10_G(x1, x2) = U10_G(x1, x2)
U11_G(x1, x2) = U11_G(x1, x2)
U6_GGA(x1, x2, x3, x4) = U6_GGA(x1, x2, x4)
ADDZE_IN_GGA(x1, x2, x3) = ADDZE_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3, x4) = U12_GGA(x1, x2, x4)
U13_GGA(x1, x2) = U13_GGA(x1, x2)
U14_GGA(x1, x2) = U14_GGA(x1, x2)
U15_GGA(x1, x2, x3, x4) = U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4) = U16_GGA(x1, x2, x4)
ADDYF_IN_GGA(x1, x2, x3) = ADDYF_IN_GGA(x1, x2)
U33_GGA(x1, x2) = U33_GGA(x1, x2)
U34_GGA(x1, x2) = U34_GGA(x1, x2)
U35_GGA(x1, x2, x3, x4) = U35_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4) = U17_GGA(x1, x2, x4)
ADDCH_IN_GGA(x1, x2, x3) = ADDCH_IN_GGA(x1, x2)
U30_GGA(x1, x2, x3) = U30_GGA(x1, x3)
SUCCZJ_IN_GA(x1, x2) = SUCCZJ_IN_GA(x1)
U20_GA(x1, x2) = U20_GA(x1, x2)
U21_GA(x1, x2, x3) = U21_GA(x1, x3)
SUCCI_IN_GA(x1, x2) = SUCCI_IN_GA(x1)
U18_GA(x1, x2) = U18_GA(x1, x2)
U19_GA(x1, x2, x3) = U19_GA(x1, x3)
U31_GGA(x1, x2, x3) = U31_GGA(x1, x3)
U32_GGA(x1, x2, x3, x4) = U32_GGA(x1, x2, x4)
ADDCK_IN_GGA(x1, x2, x3) = ADDCK_IN_GGA(x1, x2)
U22_GGA(x1, x2, x3, x4) = U22_GGA(x1, x2, x4)
U23_GGA(x1, x2) = U23_GGA(x1, x2)
U24_GGA(x1, x2, x3) = U24_GGA(x1, x3)
U25_GGA(x1, x2, x3, x4) = U25_GGA(x1, x2, x4)
U26_GGA(x1, x2) = U26_GGA(x1, x2)
U27_GGA(x1, x2, x3) = U27_GGA(x1, x3)
U28_GGA(x1, x2, x3, x4) = U28_GGA(x1, x2, x4)
U29_GGA(x1, x2, x3, x4) = U29_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4) = U7_GGA(x1, x2, x4)
U38_GGA(x1, x2, x3, x4) = U38_GGA(x1, x2, x4)
U39_GGA(x1, x2, x3, x4) = U39_GGA(x1, x2, x4)
U40_GGA(x1, x2, x3) = U40_GGA(x1, x3)
U41_GGA(x1, x2, x3, x4) = U41_GGA(x1, x2, x4)
U42_GGA(x1, x2, x3, x4) = U42_GGA(x1, x2, x4)
U43_GGA(x1, x2, x3, x4) = U43_GGA(x1, x2, x4)
U44_GGA(x1, x2, x3, x4) = U44_GGA(x1, x2, x4)
U45_GGA(x1, x2, x3, x4) = U45_GGA(x1, x2, x4)
U46_GGA(x1, x2, x3, x4) = U46_GGA(x1, x2, x4)
U47_GGA(x1, x2, x3, x4) = U47_GGA(x1, x2, x4)
U48_GGA(x1, x2, x3, x4) = U48_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESA_IN_GGA(zero(zero(X1)), X2, zero(zero(X3))) → U36_GGA(X1, X2, X3, timesA_in_gga(X1, X2, X3))
TIMESA_IN_GGA(zero(zero(X1)), X2, zero(zero(X3))) → TIMESA_IN_GGA(X1, X2, X3)
TIMESA_IN_GGA(zero(one(X1)), X2, zero(X3)) → U37_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X4))
TIMESA_IN_GGA(zero(one(X1)), X2, zero(X3)) → TIMESC_IN_GGA(X1, X2, X4)
TIMESC_IN_GGA(zero(X1), X2, zero(X3)) → U1_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X3))
TIMESC_IN_GGA(zero(X1), X2, zero(X3)) → TIMESC_IN_GGA(X1, X2, X3)
TIMESC_IN_GGA(one(X1), X2, X3) → U2_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X4))
TIMESC_IN_GGA(one(X1), X2, X3) → TIMESC_IN_GGA(X1, X2, X4)
TIMESC_IN_GGA(one(X1), X2, X3) → U3_GGA(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U3_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U4_GGA(X1, X2, X3, addB_in_gga(X2, X4, X3))
U3_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → ADDB_IN_GGA(X2, X4, X3)
ADDB_IN_GGA(b, X1, zero(X1)) → U5_GGA(X1, binaryZD_in_g(X1))
ADDB_IN_GGA(b, X1, zero(X1)) → BINARYZD_IN_G(X1)
BINARYZD_IN_G(zero(X1)) → U8_G(X1, binaryZD_in_g(X1))
BINARYZD_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYZD_IN_G(one(X1)) → U9_G(X1, binaryG_in_g(X1))
BINARYZD_IN_G(one(X1)) → BINARYG_IN_G(X1)
BINARYG_IN_G(zero(X1)) → U10_G(X1, binaryZD_in_g(X1))
BINARYG_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYG_IN_G(one(X1)) → U11_G(X1, binaryG_in_g(X1))
BINARYG_IN_G(one(X1)) → BINARYG_IN_G(X1)
ADDB_IN_GGA(zero(X1), X2, zero(X3)) → U6_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDB_IN_GGA(zero(X1), X2, zero(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(zero(X1), zero(X2), zero(X3)) → U12_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDZE_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(zero(one(X1)), one(b), one(one(X1))) → U13_GGA(X1, binaryG_in_g(X1))
ADDZE_IN_GGA(zero(one(X1)), one(b), one(one(X1))) → BINARYG_IN_G(X1)
ADDZE_IN_GGA(zero(zero(X1)), one(b), one(zero(X1))) → U14_GGA(X1, binaryZD_in_g(X1))
ADDZE_IN_GGA(zero(zero(X1)), one(b), one(zero(X1))) → BINARYZD_IN_G(X1)
ADDZE_IN_GGA(zero(X1), one(X2), one(X3)) → U15_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDZE_IN_GGA(zero(X1), one(X2), one(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(one(X1), zero(X2), one(X3)) → U16_GGA(X1, X2, X3, addyF_in_gga(X1, X2, X3))
ADDZE_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYF_IN_GGA(X1, X2, X3)
ADDYF_IN_GGA(b, one(X1), one(X1)) → U33_GGA(X1, binaryG_in_g(X1))
ADDYF_IN_GGA(b, one(X1), one(X1)) → BINARYG_IN_G(X1)
ADDYF_IN_GGA(b, zero(X1), zero(X1)) → U34_GGA(X1, binaryZD_in_g(X1))
ADDYF_IN_GGA(b, zero(X1), zero(X1)) → BINARYZD_IN_G(X1)
ADDYF_IN_GGA(X1, X2, X3) → U35_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDYF_IN_GGA(X1, X2, X3) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(one(X1), one(X2), zero(X3)) → U17_GGA(X1, X2, X3, addcH_in_gga(X1, X2, X3))
ADDZE_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCH_IN_GGA(X1, X2, X3)
ADDCH_IN_GGA(X1, b, X2) → U30_GGA(X1, X2, succZJ_in_ga(X1, X2))
ADDCH_IN_GGA(X1, b, X2) → SUCCZJ_IN_GA(X1, X2)
SUCCZJ_IN_GA(zero(X1), one(X1)) → U20_GA(X1, binaryZD_in_g(X1))
SUCCZJ_IN_GA(zero(X1), one(X1)) → BINARYZD_IN_G(X1)
SUCCZJ_IN_GA(one(X1), zero(X2)) → U21_GA(X1, X2, succI_in_ga(X1, X2))
SUCCZJ_IN_GA(one(X1), zero(X2)) → SUCCI_IN_GA(X1, X2)
SUCCI_IN_GA(zero(X1), one(X1)) → U18_GA(X1, binaryZD_in_g(X1))
SUCCI_IN_GA(zero(X1), one(X1)) → BINARYZD_IN_G(X1)
SUCCI_IN_GA(one(X1), zero(X2)) → U19_GA(X1, X2, succI_in_ga(X1, X2))
SUCCI_IN_GA(one(X1), zero(X2)) → SUCCI_IN_GA(X1, X2)
ADDCH_IN_GGA(b, X1, X2) → U31_GGA(X1, X2, succZJ_in_ga(X1, X2))
ADDCH_IN_GGA(b, X1, X2) → SUCCZJ_IN_GA(X1, X2)
ADDCH_IN_GGA(X1, X2, X3) → U32_GGA(X1, X2, X3, addCK_in_gga(X1, X2, X3))
ADDCH_IN_GGA(X1, X2, X3) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(zero(X1), zero(X2), one(X3)) → U22_GGA(X1, X2, X3, addzE_in_gga(X1, X2, X3))
ADDCK_IN_GGA(zero(X1), zero(X2), one(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(zero(zero(X1)), one(b), zero(one(X1))) → U23_GGA(X1, binaryZD_in_g(X1))
ADDCK_IN_GGA(zero(zero(X1)), one(b), zero(one(X1))) → BINARYZD_IN_G(X1)
ADDCK_IN_GGA(zero(one(X1)), one(b), zero(zero(X2))) → U24_GGA(X1, X2, succI_in_ga(X1, X2))
ADDCK_IN_GGA(zero(one(X1)), one(b), zero(zero(X2))) → SUCCI_IN_GA(X1, X2)
ADDCK_IN_GGA(zero(X1), one(X2), zero(X3)) → U25_GGA(X1, X2, X3, addCK_in_gga(X1, X2, X3))
ADDCK_IN_GGA(zero(X1), one(X2), zero(X3)) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(one(b), zero(zero(X1)), zero(one(X1))) → U26_GGA(X1, binaryZD_in_g(X1))
ADDCK_IN_GGA(one(b), zero(zero(X1)), zero(one(X1))) → BINARYZD_IN_G(X1)
ADDCK_IN_GGA(one(b), zero(one(X1)), zero(zero(X2))) → U27_GGA(X1, X2, succI_in_ga(X1, X2))
ADDCK_IN_GGA(one(b), zero(one(X1)), zero(zero(X2))) → SUCCI_IN_GA(X1, X2)
ADDCK_IN_GGA(one(X1), zero(X2), zero(X3)) → U28_GGA(X1, X2, X3, addCK_in_gga(X1, X2, X3))
ADDCK_IN_GGA(one(X1), zero(X2), zero(X3)) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(one(X1), one(X2), one(X3)) → U29_GGA(X1, X2, X3, addcH_in_gga(X1, X2, X3))
ADDCK_IN_GGA(one(X1), one(X2), one(X3)) → ADDCH_IN_GGA(X1, X2, X3)
ADDB_IN_GGA(one(X1), X2, one(X3)) → U7_GGA(X1, X2, X3, addyF_in_gga(X1, X2, X3))
ADDB_IN_GGA(one(X1), X2, one(X3)) → ADDYF_IN_GGA(X1, X2, X3)
TIMESA_IN_GGA(zero(one(X1)), X2, zero(X3)) → U38_GGA(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U38_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U39_GGA(X1, X2, X3, addB_in_gga(X2, X4, X3))
U38_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → ADDB_IN_GGA(X2, X4, X3)
TIMESA_IN_GGA(one(one(b)), X1, X2) → U40_GGA(X1, X2, addB_in_gga(X1, X1, X2))
TIMESA_IN_GGA(one(one(b)), X1, X2) → ADDB_IN_GGA(X1, X1, X2)
TIMESA_IN_GGA(one(zero(X1)), X2, X3) → U41_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X4))
TIMESA_IN_GGA(one(zero(X1)), X2, X3) → TIMESC_IN_GGA(X1, X2, X4)
TIMESA_IN_GGA(one(zero(X1)), X2, X3) → U42_GGA(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U42_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U43_GGA(X1, X2, X3, addB_in_gga(X2, zero(X4), X3))
U42_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → ADDB_IN_GGA(X2, zero(X4), X3)
TIMESA_IN_GGA(one(one(X1)), X2, X3) → U44_GGA(X1, X2, X3, timesC_in_gga(X1, X2, X4))
TIMESA_IN_GGA(one(one(X1)), X2, X3) → TIMESC_IN_GGA(X1, X2, X4)
TIMESA_IN_GGA(one(one(X1)), X2, X3) → U45_GGA(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U45_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U46_GGA(X1, X2, X3, addB_in_gga(X2, X4, X5))
U45_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → ADDB_IN_GGA(X2, X4, X5)
U45_GGA(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U47_GGA(X1, X2, X3, addcB_in_gga(X2, X4, X5))
U47_GGA(X1, X2, X3, addcB_out_gga(X2, X4, X5)) → U48_GGA(X1, X2, X3, addB_in_gga(X2, X5, X3))
U47_GGA(X1, X2, X3, addcB_out_gga(X2, X4, X5)) → ADDB_IN_GGA(X2, X5, X3)

The TRS R consists of the following rules:

timescC_in_gga(one(b), X1, X1) → timescC_out_gga(one(b), X1, X1)
timescC_in_gga(zero(X1), X2, zero(X3)) → U59_gga(X1, X2, X3, timescC_in_gga(X1, X2, X3))
timescC_in_gga(one(X1), X2, X3) → U60_gga(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U60_gga(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U61_gga(X1, X2, X3, addcB_in_gga(X2, X4, X3))
addcB_in_gga(b, X1, zero(X1)) → U62_gga(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(zero(X1)) → U65_g(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(one(X1)) → U66_g(X1, binarycG_in_g(X1))
binarycG_in_g(b) → binarycG_out_g(b)
binarycG_in_g(zero(X1)) → U67_g(X1, binaryZcD_in_g(X1))
U67_g(X1, binaryZcD_out_g(X1)) → binarycG_out_g(zero(X1))
binarycG_in_g(one(X1)) → U68_g(X1, binarycG_in_g(X1))
U68_g(X1, binarycG_out_g(X1)) → binarycG_out_g(one(X1))
U66_g(X1, binarycG_out_g(X1)) → binaryZcD_out_g(one(X1))
U65_g(X1, binaryZcD_out_g(X1)) → binaryZcD_out_g(zero(X1))
U62_gga(X1, binaryZcD_out_g(X1)) → addcB_out_gga(b, X1, zero(X1))
addcB_in_gga(zero(X1), X2, zero(X3)) → U63_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(X1), zero(X2), zero(X3)) → U69_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(one(X1)), one(b), one(one(X1))) → U70_gga(X1, binarycG_in_g(X1))
U70_gga(X1, binarycG_out_g(X1)) → addzcE_out_gga(zero(one(X1)), one(b), one(one(X1)))
addzcE_in_gga(zero(zero(X1)), one(b), one(zero(X1))) → U71_gga(X1, binaryZcD_in_g(X1))
U71_gga(X1, binaryZcD_out_g(X1)) → addzcE_out_gga(zero(zero(X1)), one(b), one(zero(X1)))
addzcE_in_gga(zero(X1), one(X2), one(X3)) → U72_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), zero(X2), one(X3)) → U73_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
addycF_in_gga(b, one(X1), one(X1)) → U90_gga(X1, binarycG_in_g(X1))
U90_gga(X1, binarycG_out_g(X1)) → addycF_out_gga(b, one(X1), one(X1))
addycF_in_gga(b, zero(X1), zero(X1)) → U91_gga(X1, binaryZcD_in_g(X1))
U91_gga(X1, binaryZcD_out_g(X1)) → addycF_out_gga(b, zero(X1), zero(X1))
addycF_in_gga(X1, X2, X3) → U92_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), one(X2), zero(X3)) → U74_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
addccH_in_gga(b, b, one(b)) → addccH_out_gga(b, b, one(b))
addccH_in_gga(X1, b, X2) → U87_gga(X1, X2, succZcJ_in_ga(X1, X2))
succZcJ_in_ga(zero(X1), one(X1)) → U77_ga(X1, binaryZcD_in_g(X1))
U77_ga(X1, binaryZcD_out_g(X1)) → succZcJ_out_ga(zero(X1), one(X1))
succZcJ_in_ga(one(X1), zero(X2)) → U78_ga(X1, X2, succcI_in_ga(X1, X2))
succcI_in_ga(b, one(b)) → succcI_out_ga(b, one(b))
succcI_in_ga(zero(X1), one(X1)) → U75_ga(X1, binaryZcD_in_g(X1))
U75_ga(X1, binaryZcD_out_g(X1)) → succcI_out_ga(zero(X1), one(X1))
succcI_in_ga(one(X1), zero(X2)) → U76_ga(X1, X2, succcI_in_ga(X1, X2))
U76_ga(X1, X2, succcI_out_ga(X1, X2)) → succcI_out_ga(one(X1), zero(X2))
U78_ga(X1, X2, succcI_out_ga(X1, X2)) → succZcJ_out_ga(one(X1), zero(X2))
U87_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(X1, b, X2)
addccH_in_gga(b, X1, X2) → U88_gga(X1, X2, succZcJ_in_ga(X1, X2))
U88_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(b, X1, X2)
addccH_in_gga(X1, X2, X3) → U89_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(zero(X1), zero(X2), one(X3)) → U79_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
U79_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), zero(X2), one(X3))
addCcK_in_gga(zero(zero(X1)), one(b), zero(one(X1))) → U80_gga(X1, binaryZcD_in_g(X1))
U80_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(zero(zero(X1)), one(b), zero(one(X1)))
addCcK_in_gga(zero(one(X1)), one(b), zero(zero(X2))) → U81_gga(X1, X2, succcI_in_ga(X1, X2))
U81_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(zero(one(X1)), one(b), zero(zero(X2)))
addCcK_in_gga(zero(X1), one(X2), zero(X3)) → U82_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(b), zero(zero(X1)), zero(one(X1))) → U83_gga(X1, binaryZcD_in_g(X1))
U83_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(one(b), zero(zero(X1)), zero(one(X1)))
addCcK_in_gga(one(b), zero(one(X1)), zero(zero(X2))) → U84_gga(X1, X2, succcI_in_ga(X1, X2))
U84_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(one(b), zero(one(X1)), zero(zero(X2)))
addCcK_in_gga(one(X1), zero(X2), zero(X3)) → U85_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(X1), one(X2), one(X3)) → U86_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
U86_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), one(X2), one(X3))
U85_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), zero(X2), zero(X3))
U82_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), one(X2), zero(X3))
U89_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addccH_out_gga(X1, X2, X3)
U74_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), one(X2), zero(X3))
U92_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addycF_out_gga(X1, X2, X3)
U73_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), zero(X2), one(X3))
U72_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), one(X2), one(X3))
U69_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), zero(X2), zero(X3))
U63_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addcB_out_gga(zero(X1), X2, zero(X3))
addcB_in_gga(one(X1), X2, one(X3)) → U64_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
U64_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addcB_out_gga(one(X1), X2, one(X3))
U61_gga(X1, X2, X3, addcB_out_gga(X2, X4, X3)) → timescC_out_gga(one(X1), X2, X3)
U59_gga(X1, X2, X3, timescC_out_gga(X1, X2, X3)) → timescC_out_gga(zero(X1), X2, zero(X3))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 73 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BINARYZD_IN_G(one(X1)) → BINARYG_IN_G(X1)
BINARYG_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYZD_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYG_IN_G(one(X1)) → BINARYG_IN_G(X1)

The TRS R consists of the following rules:

timescC_in_gga(one(b), X1, X1) → timescC_out_gga(one(b), X1, X1)
timescC_in_gga(zero(X1), X2, zero(X3)) → U59_gga(X1, X2, X3, timescC_in_gga(X1, X2, X3))
timescC_in_gga(one(X1), X2, X3) → U60_gga(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U60_gga(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U61_gga(X1, X2, X3, addcB_in_gga(X2, X4, X3))
addcB_in_gga(b, X1, zero(X1)) → U62_gga(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(zero(X1)) → U65_g(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(one(X1)) → U66_g(X1, binarycG_in_g(X1))
binarycG_in_g(b) → binarycG_out_g(b)
binarycG_in_g(zero(X1)) → U67_g(X1, binaryZcD_in_g(X1))
U67_g(X1, binaryZcD_out_g(X1)) → binarycG_out_g(zero(X1))
binarycG_in_g(one(X1)) → U68_g(X1, binarycG_in_g(X1))
U68_g(X1, binarycG_out_g(X1)) → binarycG_out_g(one(X1))
U66_g(X1, binarycG_out_g(X1)) → binaryZcD_out_g(one(X1))
U65_g(X1, binaryZcD_out_g(X1)) → binaryZcD_out_g(zero(X1))
U62_gga(X1, binaryZcD_out_g(X1)) → addcB_out_gga(b, X1, zero(X1))
addcB_in_gga(zero(X1), X2, zero(X3)) → U63_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(X1), zero(X2), zero(X3)) → U69_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(one(X1)), one(b), one(one(X1))) → U70_gga(X1, binarycG_in_g(X1))
U70_gga(X1, binarycG_out_g(X1)) → addzcE_out_gga(zero(one(X1)), one(b), one(one(X1)))
addzcE_in_gga(zero(zero(X1)), one(b), one(zero(X1))) → U71_gga(X1, binaryZcD_in_g(X1))
U71_gga(X1, binaryZcD_out_g(X1)) → addzcE_out_gga(zero(zero(X1)), one(b), one(zero(X1)))
addzcE_in_gga(zero(X1), one(X2), one(X3)) → U72_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), zero(X2), one(X3)) → U73_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
addycF_in_gga(b, one(X1), one(X1)) → U90_gga(X1, binarycG_in_g(X1))
U90_gga(X1, binarycG_out_g(X1)) → addycF_out_gga(b, one(X1), one(X1))
addycF_in_gga(b, zero(X1), zero(X1)) → U91_gga(X1, binaryZcD_in_g(X1))
U91_gga(X1, binaryZcD_out_g(X1)) → addycF_out_gga(b, zero(X1), zero(X1))
addycF_in_gga(X1, X2, X3) → U92_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), one(X2), zero(X3)) → U74_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
addccH_in_gga(b, b, one(b)) → addccH_out_gga(b, b, one(b))
addccH_in_gga(X1, b, X2) → U87_gga(X1, X2, succZcJ_in_ga(X1, X2))
succZcJ_in_ga(zero(X1), one(X1)) → U77_ga(X1, binaryZcD_in_g(X1))
U77_ga(X1, binaryZcD_out_g(X1)) → succZcJ_out_ga(zero(X1), one(X1))
succZcJ_in_ga(one(X1), zero(X2)) → U78_ga(X1, X2, succcI_in_ga(X1, X2))
succcI_in_ga(b, one(b)) → succcI_out_ga(b, one(b))
succcI_in_ga(zero(X1), one(X1)) → U75_ga(X1, binaryZcD_in_g(X1))
U75_ga(X1, binaryZcD_out_g(X1)) → succcI_out_ga(zero(X1), one(X1))
succcI_in_ga(one(X1), zero(X2)) → U76_ga(X1, X2, succcI_in_ga(X1, X2))
U76_ga(X1, X2, succcI_out_ga(X1, X2)) → succcI_out_ga(one(X1), zero(X2))
U78_ga(X1, X2, succcI_out_ga(X1, X2)) → succZcJ_out_ga(one(X1), zero(X2))
U87_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(X1, b, X2)
addccH_in_gga(b, X1, X2) → U88_gga(X1, X2, succZcJ_in_ga(X1, X2))
U88_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(b, X1, X2)
addccH_in_gga(X1, X2, X3) → U89_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(zero(X1), zero(X2), one(X3)) → U79_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
U79_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), zero(X2), one(X3))
addCcK_in_gga(zero(zero(X1)), one(b), zero(one(X1))) → U80_gga(X1, binaryZcD_in_g(X1))
U80_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(zero(zero(X1)), one(b), zero(one(X1)))
addCcK_in_gga(zero(one(X1)), one(b), zero(zero(X2))) → U81_gga(X1, X2, succcI_in_ga(X1, X2))
U81_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(zero(one(X1)), one(b), zero(zero(X2)))
addCcK_in_gga(zero(X1), one(X2), zero(X3)) → U82_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(b), zero(zero(X1)), zero(one(X1))) → U83_gga(X1, binaryZcD_in_g(X1))
U83_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(one(b), zero(zero(X1)), zero(one(X1)))
addCcK_in_gga(one(b), zero(one(X1)), zero(zero(X2))) → U84_gga(X1, X2, succcI_in_ga(X1, X2))
U84_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(one(b), zero(one(X1)), zero(zero(X2)))
addCcK_in_gga(one(X1), zero(X2), zero(X3)) → U85_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(X1), one(X2), one(X3)) → U86_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
U86_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), one(X2), one(X3))
U85_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), zero(X2), zero(X3))
U82_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), one(X2), zero(X3))
U89_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addccH_out_gga(X1, X2, X3)
U74_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), one(X2), zero(X3))
U92_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addycF_out_gga(X1, X2, X3)
U73_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), zero(X2), one(X3))
U72_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), one(X2), one(X3))
U69_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), zero(X2), zero(X3))
U63_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addcB_out_gga(zero(X1), X2, zero(X3))
addcB_in_gga(one(X1), X2, one(X3)) → U64_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
U64_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addcB_out_gga(one(X1), X2, one(X3))
U61_gga(X1, X2, X3, addcB_out_gga(X2, X4, X3)) → timescC_out_gga(one(X1), X2, X3)
U59_gga(X1, X2, X3, timescC_out_gga(X1, X2, X3)) → timescC_out_gga(zero(X1), X2, zero(X3))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timescC_in_gga(x1, x2, x3) = timescC_in_gga(x1, x2)
b = b
timescC_out_gga(x1, x2, x3) = timescC_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addcB_in_gga(x1, x2, x3) = addcB_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZcD_in_g(x1) = binaryZcD_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binarycG_in_g(x1) = binarycG_in_g(x1)
binarycG_out_g(x1) = binarycG_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZcD_out_g(x1) = binaryZcD_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addcB_out_gga(x1, x2, x3) = addcB_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzcE_in_gga(x1, x2, x3) = addzcE_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzcE_out_gga(x1, x2, x3) = addzcE_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addycF_in_gga(x1, x2, x3) = addycF_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addycF_out_gga(x1, x2, x3) = addycF_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addccH_in_gga(x1, x2, x3) = addccH_in_gga(x1, x2)
addccH_out_gga(x1, x2, x3) = addccH_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZcJ_in_ga(x1, x2) = succZcJ_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZcJ_out_ga(x1, x2) = succZcJ_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succcI_in_ga(x1, x2) = succcI_in_ga(x1)
succcI_out_ga(x1, x2) = succcI_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCcK_in_gga(x1, x2, x3) = addCcK_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCcK_out_gga(x1, x2, x3) = addCcK_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
BINARYZD_IN_G(x1) = BINARYZD_IN_G(x1)
BINARYG_IN_G(x1) = BINARYG_IN_G(x1)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BINARYZD_IN_G(one(X1)) → BINARYG_IN_G(X1)
BINARYG_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYZD_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYG_IN_G(one(X1)) → BINARYG_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BINARYZD_IN_G(one(X1)) → BINARYG_IN_G(X1)
BINARYG_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYZD_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
BINARYG_IN_G(one(X1)) → BINARYG_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

BINARYG_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
The graph contains the following edges 1 > 1
BINARYG_IN_G(one(X1)) → BINARYG_IN_G(X1)
The graph contains the following edges 1 > 1
BINARYZD_IN_G(zero(X1)) → BINARYZD_IN_G(X1)
The graph contains the following edges 1 > 1
BINARYZD_IN_G(one(X1)) → BINARYG_IN_G(X1)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUCCI_IN_GA(one(X1), zero(X2)) → SUCCI_IN_GA(X1, X2)

The TRS R consists of the following rules:

timescC_in_gga(one(b), X1, X1) → timescC_out_gga(one(b), X1, X1)
timescC_in_gga(zero(X1), X2, zero(X3)) → U59_gga(X1, X2, X3, timescC_in_gga(X1, X2, X3))
timescC_in_gga(one(X1), X2, X3) → U60_gga(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U60_gga(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U61_gga(X1, X2, X3, addcB_in_gga(X2, X4, X3))
addcB_in_gga(b, X1, zero(X1)) → U62_gga(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(zero(X1)) → U65_g(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(one(X1)) → U66_g(X1, binarycG_in_g(X1))
binarycG_in_g(b) → binarycG_out_g(b)
binarycG_in_g(zero(X1)) → U67_g(X1, binaryZcD_in_g(X1))
U67_g(X1, binaryZcD_out_g(X1)) → binarycG_out_g(zero(X1))
binarycG_in_g(one(X1)) → U68_g(X1, binarycG_in_g(X1))
U68_g(X1, binarycG_out_g(X1)) → binarycG_out_g(one(X1))
U66_g(X1, binarycG_out_g(X1)) → binaryZcD_out_g(one(X1))
U65_g(X1, binaryZcD_out_g(X1)) → binaryZcD_out_g(zero(X1))
U62_gga(X1, binaryZcD_out_g(X1)) → addcB_out_gga(b, X1, zero(X1))
addcB_in_gga(zero(X1), X2, zero(X3)) → U63_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(X1), zero(X2), zero(X3)) → U69_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(one(X1)), one(b), one(one(X1))) → U70_gga(X1, binarycG_in_g(X1))
U70_gga(X1, binarycG_out_g(X1)) → addzcE_out_gga(zero(one(X1)), one(b), one(one(X1)))
addzcE_in_gga(zero(zero(X1)), one(b), one(zero(X1))) → U71_gga(X1, binaryZcD_in_g(X1))
U71_gga(X1, binaryZcD_out_g(X1)) → addzcE_out_gga(zero(zero(X1)), one(b), one(zero(X1)))
addzcE_in_gga(zero(X1), one(X2), one(X3)) → U72_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), zero(X2), one(X3)) → U73_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
addycF_in_gga(b, one(X1), one(X1)) → U90_gga(X1, binarycG_in_g(X1))
U90_gga(X1, binarycG_out_g(X1)) → addycF_out_gga(b, one(X1), one(X1))
addycF_in_gga(b, zero(X1), zero(X1)) → U91_gga(X1, binaryZcD_in_g(X1))
U91_gga(X1, binaryZcD_out_g(X1)) → addycF_out_gga(b, zero(X1), zero(X1))
addycF_in_gga(X1, X2, X3) → U92_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), one(X2), zero(X3)) → U74_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
addccH_in_gga(b, b, one(b)) → addccH_out_gga(b, b, one(b))
addccH_in_gga(X1, b, X2) → U87_gga(X1, X2, succZcJ_in_ga(X1, X2))
succZcJ_in_ga(zero(X1), one(X1)) → U77_ga(X1, binaryZcD_in_g(X1))
U77_ga(X1, binaryZcD_out_g(X1)) → succZcJ_out_ga(zero(X1), one(X1))
succZcJ_in_ga(one(X1), zero(X2)) → U78_ga(X1, X2, succcI_in_ga(X1, X2))
succcI_in_ga(b, one(b)) → succcI_out_ga(b, one(b))
succcI_in_ga(zero(X1), one(X1)) → U75_ga(X1, binaryZcD_in_g(X1))
U75_ga(X1, binaryZcD_out_g(X1)) → succcI_out_ga(zero(X1), one(X1))
succcI_in_ga(one(X1), zero(X2)) → U76_ga(X1, X2, succcI_in_ga(X1, X2))
U76_ga(X1, X2, succcI_out_ga(X1, X2)) → succcI_out_ga(one(X1), zero(X2))
U78_ga(X1, X2, succcI_out_ga(X1, X2)) → succZcJ_out_ga(one(X1), zero(X2))
U87_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(X1, b, X2)
addccH_in_gga(b, X1, X2) → U88_gga(X1, X2, succZcJ_in_ga(X1, X2))
U88_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(b, X1, X2)
addccH_in_gga(X1, X2, X3) → U89_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(zero(X1), zero(X2), one(X3)) → U79_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
U79_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), zero(X2), one(X3))
addCcK_in_gga(zero(zero(X1)), one(b), zero(one(X1))) → U80_gga(X1, binaryZcD_in_g(X1))
U80_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(zero(zero(X1)), one(b), zero(one(X1)))
addCcK_in_gga(zero(one(X1)), one(b), zero(zero(X2))) → U81_gga(X1, X2, succcI_in_ga(X1, X2))
U81_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(zero(one(X1)), one(b), zero(zero(X2)))
addCcK_in_gga(zero(X1), one(X2), zero(X3)) → U82_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(b), zero(zero(X1)), zero(one(X1))) → U83_gga(X1, binaryZcD_in_g(X1))
U83_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(one(b), zero(zero(X1)), zero(one(X1)))
addCcK_in_gga(one(b), zero(one(X1)), zero(zero(X2))) → U84_gga(X1, X2, succcI_in_ga(X1, X2))
U84_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(one(b), zero(one(X1)), zero(zero(X2)))
addCcK_in_gga(one(X1), zero(X2), zero(X3)) → U85_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(X1), one(X2), one(X3)) → U86_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
U86_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), one(X2), one(X3))
U85_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), zero(X2), zero(X3))
U82_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), one(X2), zero(X3))
U89_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addccH_out_gga(X1, X2, X3)
U74_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), one(X2), zero(X3))
U92_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addycF_out_gga(X1, X2, X3)
U73_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), zero(X2), one(X3))
U72_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), one(X2), one(X3))
U69_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), zero(X2), zero(X3))
U63_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addcB_out_gga(zero(X1), X2, zero(X3))
addcB_in_gga(one(X1), X2, one(X3)) → U64_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
U64_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addcB_out_gga(one(X1), X2, one(X3))
U61_gga(X1, X2, X3, addcB_out_gga(X2, X4, X3)) → timescC_out_gga(one(X1), X2, X3)
U59_gga(X1, X2, X3, timescC_out_gga(X1, X2, X3)) → timescC_out_gga(zero(X1), X2, zero(X3))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timescC_in_gga(x1, x2, x3) = timescC_in_gga(x1, x2)
b = b
timescC_out_gga(x1, x2, x3) = timescC_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addcB_in_gga(x1, x2, x3) = addcB_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZcD_in_g(x1) = binaryZcD_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binarycG_in_g(x1) = binarycG_in_g(x1)
binarycG_out_g(x1) = binarycG_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZcD_out_g(x1) = binaryZcD_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addcB_out_gga(x1, x2, x3) = addcB_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzcE_in_gga(x1, x2, x3) = addzcE_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzcE_out_gga(x1, x2, x3) = addzcE_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addycF_in_gga(x1, x2, x3) = addycF_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addycF_out_gga(x1, x2, x3) = addycF_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addccH_in_gga(x1, x2, x3) = addccH_in_gga(x1, x2)
addccH_out_gga(x1, x2, x3) = addccH_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZcJ_in_ga(x1, x2) = succZcJ_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZcJ_out_ga(x1, x2) = succZcJ_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succcI_in_ga(x1, x2) = succcI_in_ga(x1)
succcI_out_ga(x1, x2) = succcI_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCcK_in_gga(x1, x2, x3) = addCcK_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCcK_out_gga(x1, x2, x3) = addCcK_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
SUCCI_IN_GA(x1, x2) = SUCCI_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUCCI_IN_GA(one(X1), zero(X2)) → SUCCI_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
SUCCI_IN_GA(x1, x2) = SUCCI_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUCCI_IN_GA(one(X1)) → SUCCI_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

SUCCI_IN_GA(one(X1)) → SUCCI_IN_GA(X1)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDZE_IN_GGA(zero(X1), one(X2), one(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYF_IN_GGA(X1, X2, X3)
ADDYF_IN_GGA(X1, X2, X3) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCH_IN_GGA(X1, X2, X3)
ADDCH_IN_GGA(X1, X2, X3) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(zero(X1), zero(X2), one(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(zero(X1), one(X2), zero(X3)) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(one(X1), zero(X2), zero(X3)) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(one(X1), one(X2), one(X3)) → ADDCH_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

timescC_in_gga(one(b), X1, X1) → timescC_out_gga(one(b), X1, X1)
timescC_in_gga(zero(X1), X2, zero(X3)) → U59_gga(X1, X2, X3, timescC_in_gga(X1, X2, X3))
timescC_in_gga(one(X1), X2, X3) → U60_gga(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U60_gga(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U61_gga(X1, X2, X3, addcB_in_gga(X2, X4, X3))
addcB_in_gga(b, X1, zero(X1)) → U62_gga(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(zero(X1)) → U65_g(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(one(X1)) → U66_g(X1, binarycG_in_g(X1))
binarycG_in_g(b) → binarycG_out_g(b)
binarycG_in_g(zero(X1)) → U67_g(X1, binaryZcD_in_g(X1))
U67_g(X1, binaryZcD_out_g(X1)) → binarycG_out_g(zero(X1))
binarycG_in_g(one(X1)) → U68_g(X1, binarycG_in_g(X1))
U68_g(X1, binarycG_out_g(X1)) → binarycG_out_g(one(X1))
U66_g(X1, binarycG_out_g(X1)) → binaryZcD_out_g(one(X1))
U65_g(X1, binaryZcD_out_g(X1)) → binaryZcD_out_g(zero(X1))
U62_gga(X1, binaryZcD_out_g(X1)) → addcB_out_gga(b, X1, zero(X1))
addcB_in_gga(zero(X1), X2, zero(X3)) → U63_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(X1), zero(X2), zero(X3)) → U69_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(one(X1)), one(b), one(one(X1))) → U70_gga(X1, binarycG_in_g(X1))
U70_gga(X1, binarycG_out_g(X1)) → addzcE_out_gga(zero(one(X1)), one(b), one(one(X1)))
addzcE_in_gga(zero(zero(X1)), one(b), one(zero(X1))) → U71_gga(X1, binaryZcD_in_g(X1))
U71_gga(X1, binaryZcD_out_g(X1)) → addzcE_out_gga(zero(zero(X1)), one(b), one(zero(X1)))
addzcE_in_gga(zero(X1), one(X2), one(X3)) → U72_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), zero(X2), one(X3)) → U73_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
addycF_in_gga(b, one(X1), one(X1)) → U90_gga(X1, binarycG_in_g(X1))
U90_gga(X1, binarycG_out_g(X1)) → addycF_out_gga(b, one(X1), one(X1))
addycF_in_gga(b, zero(X1), zero(X1)) → U91_gga(X1, binaryZcD_in_g(X1))
U91_gga(X1, binaryZcD_out_g(X1)) → addycF_out_gga(b, zero(X1), zero(X1))
addycF_in_gga(X1, X2, X3) → U92_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), one(X2), zero(X3)) → U74_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
addccH_in_gga(b, b, one(b)) → addccH_out_gga(b, b, one(b))
addccH_in_gga(X1, b, X2) → U87_gga(X1, X2, succZcJ_in_ga(X1, X2))
succZcJ_in_ga(zero(X1), one(X1)) → U77_ga(X1, binaryZcD_in_g(X1))
U77_ga(X1, binaryZcD_out_g(X1)) → succZcJ_out_ga(zero(X1), one(X1))
succZcJ_in_ga(one(X1), zero(X2)) → U78_ga(X1, X2, succcI_in_ga(X1, X2))
succcI_in_ga(b, one(b)) → succcI_out_ga(b, one(b))
succcI_in_ga(zero(X1), one(X1)) → U75_ga(X1, binaryZcD_in_g(X1))
U75_ga(X1, binaryZcD_out_g(X1)) → succcI_out_ga(zero(X1), one(X1))
succcI_in_ga(one(X1), zero(X2)) → U76_ga(X1, X2, succcI_in_ga(X1, X2))
U76_ga(X1, X2, succcI_out_ga(X1, X2)) → succcI_out_ga(one(X1), zero(X2))
U78_ga(X1, X2, succcI_out_ga(X1, X2)) → succZcJ_out_ga(one(X1), zero(X2))
U87_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(X1, b, X2)
addccH_in_gga(b, X1, X2) → U88_gga(X1, X2, succZcJ_in_ga(X1, X2))
U88_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(b, X1, X2)
addccH_in_gga(X1, X2, X3) → U89_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(zero(X1), zero(X2), one(X3)) → U79_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
U79_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), zero(X2), one(X3))
addCcK_in_gga(zero(zero(X1)), one(b), zero(one(X1))) → U80_gga(X1, binaryZcD_in_g(X1))
U80_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(zero(zero(X1)), one(b), zero(one(X1)))
addCcK_in_gga(zero(one(X1)), one(b), zero(zero(X2))) → U81_gga(X1, X2, succcI_in_ga(X1, X2))
U81_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(zero(one(X1)), one(b), zero(zero(X2)))
addCcK_in_gga(zero(X1), one(X2), zero(X3)) → U82_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(b), zero(zero(X1)), zero(one(X1))) → U83_gga(X1, binaryZcD_in_g(X1))
U83_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(one(b), zero(zero(X1)), zero(one(X1)))
addCcK_in_gga(one(b), zero(one(X1)), zero(zero(X2))) → U84_gga(X1, X2, succcI_in_ga(X1, X2))
U84_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(one(b), zero(one(X1)), zero(zero(X2)))
addCcK_in_gga(one(X1), zero(X2), zero(X3)) → U85_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(X1), one(X2), one(X3)) → U86_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
U86_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), one(X2), one(X3))
U85_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), zero(X2), zero(X3))
U82_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), one(X2), zero(X3))
U89_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addccH_out_gga(X1, X2, X3)
U74_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), one(X2), zero(X3))
U92_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addycF_out_gga(X1, X2, X3)
U73_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), zero(X2), one(X3))
U72_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), one(X2), one(X3))
U69_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), zero(X2), zero(X3))
U63_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addcB_out_gga(zero(X1), X2, zero(X3))
addcB_in_gga(one(X1), X2, one(X3)) → U64_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
U64_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addcB_out_gga(one(X1), X2, one(X3))
U61_gga(X1, X2, X3, addcB_out_gga(X2, X4, X3)) → timescC_out_gga(one(X1), X2, X3)
U59_gga(X1, X2, X3, timescC_out_gga(X1, X2, X3)) → timescC_out_gga(zero(X1), X2, zero(X3))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timescC_in_gga(x1, x2, x3) = timescC_in_gga(x1, x2)
b = b
timescC_out_gga(x1, x2, x3) = timescC_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addcB_in_gga(x1, x2, x3) = addcB_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZcD_in_g(x1) = binaryZcD_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binarycG_in_g(x1) = binarycG_in_g(x1)
binarycG_out_g(x1) = binarycG_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZcD_out_g(x1) = binaryZcD_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addcB_out_gga(x1, x2, x3) = addcB_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzcE_in_gga(x1, x2, x3) = addzcE_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzcE_out_gga(x1, x2, x3) = addzcE_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addycF_in_gga(x1, x2, x3) = addycF_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addycF_out_gga(x1, x2, x3) = addycF_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addccH_in_gga(x1, x2, x3) = addccH_in_gga(x1, x2)
addccH_out_gga(x1, x2, x3) = addccH_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZcJ_in_ga(x1, x2) = succZcJ_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZcJ_out_ga(x1, x2) = succZcJ_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succcI_in_ga(x1, x2) = succcI_in_ga(x1)
succcI_out_ga(x1, x2) = succcI_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCcK_in_gga(x1, x2, x3) = addCcK_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCcK_out_gga(x1, x2, x3) = addCcK_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
ADDZE_IN_GGA(x1, x2, x3) = ADDZE_IN_GGA(x1, x2)
ADDYF_IN_GGA(x1, x2, x3) = ADDYF_IN_GGA(x1, x2)
ADDCH_IN_GGA(x1, x2, x3) = ADDCH_IN_GGA(x1, x2)
ADDCK_IN_GGA(x1, x2, x3) = ADDCK_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADDZE_IN_GGA(zero(X1), one(X2), one(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYF_IN_GGA(X1, X2, X3)
ADDYF_IN_GGA(X1, X2, X3) → ADDZE_IN_GGA(X1, X2, X3)
ADDZE_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCH_IN_GGA(X1, X2, X3)
ADDCH_IN_GGA(X1, X2, X3) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(zero(X1), zero(X2), one(X3)) → ADDZE_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(zero(X1), one(X2), zero(X3)) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(one(X1), zero(X2), zero(X3)) → ADDCK_IN_GGA(X1, X2, X3)
ADDCK_IN_GGA(one(X1), one(X2), one(X3)) → ADDCH_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
ADDZE_IN_GGA(x1, x2, x3) = ADDZE_IN_GGA(x1, x2)
ADDYF_IN_GGA(x1, x2, x3) = ADDYF_IN_GGA(x1, x2)
ADDCH_IN_GGA(x1, x2, x3) = ADDCH_IN_GGA(x1, x2)
ADDCK_IN_GGA(x1, x2, x3) = ADDCK_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADDZE_IN_GGA(zero(X1), one(X2)) → ADDZE_IN_GGA(X1, X2)
ADDZE_IN_GGA(zero(X1), zero(X2)) → ADDZE_IN_GGA(X1, X2)
ADDZE_IN_GGA(one(X1), zero(X2)) → ADDYF_IN_GGA(X1, X2)
ADDYF_IN_GGA(X1, X2) → ADDZE_IN_GGA(X1, X2)
ADDZE_IN_GGA(one(X1), one(X2)) → ADDCH_IN_GGA(X1, X2)
ADDCH_IN_GGA(X1, X2) → ADDCK_IN_GGA(X1, X2)
ADDCK_IN_GGA(zero(X1), zero(X2)) → ADDZE_IN_GGA(X1, X2)
ADDCK_IN_GGA(zero(X1), one(X2)) → ADDCK_IN_GGA(X1, X2)
ADDCK_IN_GGA(one(X1), zero(X2)) → ADDCK_IN_GGA(X1, X2)
ADDCK_IN_GGA(one(X1), one(X2)) → ADDCH_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ADDYF_IN_GGA(X1, X2) → ADDZE_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDCK_IN_GGA(zero(X1), zero(X2)) → ADDZE_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
ADDZE_IN_GGA(one(X1), zero(X2)) → ADDYF_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
ADDZE_IN_GGA(one(X1), one(X2)) → ADDCH_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
ADDCH_IN_GGA(X1, X2) → ADDCK_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDCK_IN_GGA(one(X1), one(X2)) → ADDCH_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
ADDZE_IN_GGA(zero(X1), one(X2)) → ADDZE_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
ADDZE_IN_GGA(zero(X1), zero(X2)) → ADDZE_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
ADDCK_IN_GGA(zero(X1), one(X2)) → ADDCK_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
ADDCK_IN_GGA(one(X1), zero(X2)) → ADDCK_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESC_IN_GGA(one(X1), X2, X3) → TIMESC_IN_GGA(X1, X2, X4)
TIMESC_IN_GGA(zero(X1), X2, zero(X3)) → TIMESC_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

timescC_in_gga(one(b), X1, X1) → timescC_out_gga(one(b), X1, X1)
timescC_in_gga(zero(X1), X2, zero(X3)) → U59_gga(X1, X2, X3, timescC_in_gga(X1, X2, X3))
timescC_in_gga(one(X1), X2, X3) → U60_gga(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U60_gga(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U61_gga(X1, X2, X3, addcB_in_gga(X2, X4, X3))
addcB_in_gga(b, X1, zero(X1)) → U62_gga(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(zero(X1)) → U65_g(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(one(X1)) → U66_g(X1, binarycG_in_g(X1))
binarycG_in_g(b) → binarycG_out_g(b)
binarycG_in_g(zero(X1)) → U67_g(X1, binaryZcD_in_g(X1))
U67_g(X1, binaryZcD_out_g(X1)) → binarycG_out_g(zero(X1))
binarycG_in_g(one(X1)) → U68_g(X1, binarycG_in_g(X1))
U68_g(X1, binarycG_out_g(X1)) → binarycG_out_g(one(X1))
U66_g(X1, binarycG_out_g(X1)) → binaryZcD_out_g(one(X1))
U65_g(X1, binaryZcD_out_g(X1)) → binaryZcD_out_g(zero(X1))
U62_gga(X1, binaryZcD_out_g(X1)) → addcB_out_gga(b, X1, zero(X1))
addcB_in_gga(zero(X1), X2, zero(X3)) → U63_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(X1), zero(X2), zero(X3)) → U69_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(one(X1)), one(b), one(one(X1))) → U70_gga(X1, binarycG_in_g(X1))
U70_gga(X1, binarycG_out_g(X1)) → addzcE_out_gga(zero(one(X1)), one(b), one(one(X1)))
addzcE_in_gga(zero(zero(X1)), one(b), one(zero(X1))) → U71_gga(X1, binaryZcD_in_g(X1))
U71_gga(X1, binaryZcD_out_g(X1)) → addzcE_out_gga(zero(zero(X1)), one(b), one(zero(X1)))
addzcE_in_gga(zero(X1), one(X2), one(X3)) → U72_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), zero(X2), one(X3)) → U73_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
addycF_in_gga(b, one(X1), one(X1)) → U90_gga(X1, binarycG_in_g(X1))
U90_gga(X1, binarycG_out_g(X1)) → addycF_out_gga(b, one(X1), one(X1))
addycF_in_gga(b, zero(X1), zero(X1)) → U91_gga(X1, binaryZcD_in_g(X1))
U91_gga(X1, binaryZcD_out_g(X1)) → addycF_out_gga(b, zero(X1), zero(X1))
addycF_in_gga(X1, X2, X3) → U92_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), one(X2), zero(X3)) → U74_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
addccH_in_gga(b, b, one(b)) → addccH_out_gga(b, b, one(b))
addccH_in_gga(X1, b, X2) → U87_gga(X1, X2, succZcJ_in_ga(X1, X2))
succZcJ_in_ga(zero(X1), one(X1)) → U77_ga(X1, binaryZcD_in_g(X1))
U77_ga(X1, binaryZcD_out_g(X1)) → succZcJ_out_ga(zero(X1), one(X1))
succZcJ_in_ga(one(X1), zero(X2)) → U78_ga(X1, X2, succcI_in_ga(X1, X2))
succcI_in_ga(b, one(b)) → succcI_out_ga(b, one(b))
succcI_in_ga(zero(X1), one(X1)) → U75_ga(X1, binaryZcD_in_g(X1))
U75_ga(X1, binaryZcD_out_g(X1)) → succcI_out_ga(zero(X1), one(X1))
succcI_in_ga(one(X1), zero(X2)) → U76_ga(X1, X2, succcI_in_ga(X1, X2))
U76_ga(X1, X2, succcI_out_ga(X1, X2)) → succcI_out_ga(one(X1), zero(X2))
U78_ga(X1, X2, succcI_out_ga(X1, X2)) → succZcJ_out_ga(one(X1), zero(X2))
U87_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(X1, b, X2)
addccH_in_gga(b, X1, X2) → U88_gga(X1, X2, succZcJ_in_ga(X1, X2))
U88_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(b, X1, X2)
addccH_in_gga(X1, X2, X3) → U89_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(zero(X1), zero(X2), one(X3)) → U79_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
U79_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), zero(X2), one(X3))
addCcK_in_gga(zero(zero(X1)), one(b), zero(one(X1))) → U80_gga(X1, binaryZcD_in_g(X1))
U80_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(zero(zero(X1)), one(b), zero(one(X1)))
addCcK_in_gga(zero(one(X1)), one(b), zero(zero(X2))) → U81_gga(X1, X2, succcI_in_ga(X1, X2))
U81_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(zero(one(X1)), one(b), zero(zero(X2)))
addCcK_in_gga(zero(X1), one(X2), zero(X3)) → U82_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(b), zero(zero(X1)), zero(one(X1))) → U83_gga(X1, binaryZcD_in_g(X1))
U83_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(one(b), zero(zero(X1)), zero(one(X1)))
addCcK_in_gga(one(b), zero(one(X1)), zero(zero(X2))) → U84_gga(X1, X2, succcI_in_ga(X1, X2))
U84_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(one(b), zero(one(X1)), zero(zero(X2)))
addCcK_in_gga(one(X1), zero(X2), zero(X3)) → U85_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(X1), one(X2), one(X3)) → U86_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
U86_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), one(X2), one(X3))
U85_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), zero(X2), zero(X3))
U82_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), one(X2), zero(X3))
U89_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addccH_out_gga(X1, X2, X3)
U74_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), one(X2), zero(X3))
U92_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addycF_out_gga(X1, X2, X3)
U73_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), zero(X2), one(X3))
U72_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), one(X2), one(X3))
U69_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), zero(X2), zero(X3))
U63_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addcB_out_gga(zero(X1), X2, zero(X3))
addcB_in_gga(one(X1), X2, one(X3)) → U64_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
U64_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addcB_out_gga(one(X1), X2, one(X3))
U61_gga(X1, X2, X3, addcB_out_gga(X2, X4, X3)) → timescC_out_gga(one(X1), X2, X3)
U59_gga(X1, X2, X3, timescC_out_gga(X1, X2, X3)) → timescC_out_gga(zero(X1), X2, zero(X3))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timescC_in_gga(x1, x2, x3) = timescC_in_gga(x1, x2)
b = b
timescC_out_gga(x1, x2, x3) = timescC_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addcB_in_gga(x1, x2, x3) = addcB_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZcD_in_g(x1) = binaryZcD_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binarycG_in_g(x1) = binarycG_in_g(x1)
binarycG_out_g(x1) = binarycG_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZcD_out_g(x1) = binaryZcD_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addcB_out_gga(x1, x2, x3) = addcB_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzcE_in_gga(x1, x2, x3) = addzcE_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzcE_out_gga(x1, x2, x3) = addzcE_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addycF_in_gga(x1, x2, x3) = addycF_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addycF_out_gga(x1, x2, x3) = addycF_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addccH_in_gga(x1, x2, x3) = addccH_in_gga(x1, x2)
addccH_out_gga(x1, x2, x3) = addccH_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZcJ_in_ga(x1, x2) = succZcJ_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZcJ_out_ga(x1, x2) = succZcJ_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succcI_in_ga(x1, x2) = succcI_in_ga(x1)
succcI_out_ga(x1, x2) = succcI_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCcK_in_gga(x1, x2, x3) = addCcK_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCcK_out_gga(x1, x2, x3) = addCcK_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
TIMESC_IN_GGA(x1, x2, x3) = TIMESC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESC_IN_GGA(one(X1), X2, X3) → TIMESC_IN_GGA(X1, X2, X4)
TIMESC_IN_GGA(zero(X1), X2, zero(X3)) → TIMESC_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
TIMESC_IN_GGA(x1, x2, x3) = TIMESC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMESC_IN_GGA(one(X1), X2) → TIMESC_IN_GGA(X1, X2)
TIMESC_IN_GGA(zero(X1), X2) → TIMESC_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

TIMESC_IN_GGA(one(X1), X2) → TIMESC_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
TIMESC_IN_GGA(zero(X1), X2) → TIMESC_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESA_IN_GGA(zero(zero(X1)), X2, zero(zero(X3))) → TIMESA_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

timescC_in_gga(one(b), X1, X1) → timescC_out_gga(one(b), X1, X1)
timescC_in_gga(zero(X1), X2, zero(X3)) → U59_gga(X1, X2, X3, timescC_in_gga(X1, X2, X3))
timescC_in_gga(one(X1), X2, X3) → U60_gga(X1, X2, X3, timescC_in_gga(X1, X2, X4))
U60_gga(X1, X2, X3, timescC_out_gga(X1, X2, X4)) → U61_gga(X1, X2, X3, addcB_in_gga(X2, X4, X3))
addcB_in_gga(b, X1, zero(X1)) → U62_gga(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(zero(X1)) → U65_g(X1, binaryZcD_in_g(X1))
binaryZcD_in_g(one(X1)) → U66_g(X1, binarycG_in_g(X1))
binarycG_in_g(b) → binarycG_out_g(b)
binarycG_in_g(zero(X1)) → U67_g(X1, binaryZcD_in_g(X1))
U67_g(X1, binaryZcD_out_g(X1)) → binarycG_out_g(zero(X1))
binarycG_in_g(one(X1)) → U68_g(X1, binarycG_in_g(X1))
U68_g(X1, binarycG_out_g(X1)) → binarycG_out_g(one(X1))
U66_g(X1, binarycG_out_g(X1)) → binaryZcD_out_g(one(X1))
U65_g(X1, binaryZcD_out_g(X1)) → binaryZcD_out_g(zero(X1))
U62_gga(X1, binaryZcD_out_g(X1)) → addcB_out_gga(b, X1, zero(X1))
addcB_in_gga(zero(X1), X2, zero(X3)) → U63_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(X1), zero(X2), zero(X3)) → U69_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(zero(one(X1)), one(b), one(one(X1))) → U70_gga(X1, binarycG_in_g(X1))
U70_gga(X1, binarycG_out_g(X1)) → addzcE_out_gga(zero(one(X1)), one(b), one(one(X1)))
addzcE_in_gga(zero(zero(X1)), one(b), one(zero(X1))) → U71_gga(X1, binaryZcD_in_g(X1))
U71_gga(X1, binaryZcD_out_g(X1)) → addzcE_out_gga(zero(zero(X1)), one(b), one(zero(X1)))
addzcE_in_gga(zero(X1), one(X2), one(X3)) → U72_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), zero(X2), one(X3)) → U73_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
addycF_in_gga(b, one(X1), one(X1)) → U90_gga(X1, binarycG_in_g(X1))
U90_gga(X1, binarycG_out_g(X1)) → addycF_out_gga(b, one(X1), one(X1))
addycF_in_gga(b, zero(X1), zero(X1)) → U91_gga(X1, binaryZcD_in_g(X1))
U91_gga(X1, binaryZcD_out_g(X1)) → addycF_out_gga(b, zero(X1), zero(X1))
addycF_in_gga(X1, X2, X3) → U92_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
addzcE_in_gga(one(X1), one(X2), zero(X3)) → U74_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
addccH_in_gga(b, b, one(b)) → addccH_out_gga(b, b, one(b))
addccH_in_gga(X1, b, X2) → U87_gga(X1, X2, succZcJ_in_ga(X1, X2))
succZcJ_in_ga(zero(X1), one(X1)) → U77_ga(X1, binaryZcD_in_g(X1))
U77_ga(X1, binaryZcD_out_g(X1)) → succZcJ_out_ga(zero(X1), one(X1))
succZcJ_in_ga(one(X1), zero(X2)) → U78_ga(X1, X2, succcI_in_ga(X1, X2))
succcI_in_ga(b, one(b)) → succcI_out_ga(b, one(b))
succcI_in_ga(zero(X1), one(X1)) → U75_ga(X1, binaryZcD_in_g(X1))
U75_ga(X1, binaryZcD_out_g(X1)) → succcI_out_ga(zero(X1), one(X1))
succcI_in_ga(one(X1), zero(X2)) → U76_ga(X1, X2, succcI_in_ga(X1, X2))
U76_ga(X1, X2, succcI_out_ga(X1, X2)) → succcI_out_ga(one(X1), zero(X2))
U78_ga(X1, X2, succcI_out_ga(X1, X2)) → succZcJ_out_ga(one(X1), zero(X2))
U87_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(X1, b, X2)
addccH_in_gga(b, X1, X2) → U88_gga(X1, X2, succZcJ_in_ga(X1, X2))
U88_gga(X1, X2, succZcJ_out_ga(X1, X2)) → addccH_out_gga(b, X1, X2)
addccH_in_gga(X1, X2, X3) → U89_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(zero(X1), zero(X2), one(X3)) → U79_gga(X1, X2, X3, addzcE_in_gga(X1, X2, X3))
U79_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), zero(X2), one(X3))
addCcK_in_gga(zero(zero(X1)), one(b), zero(one(X1))) → U80_gga(X1, binaryZcD_in_g(X1))
U80_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(zero(zero(X1)), one(b), zero(one(X1)))
addCcK_in_gga(zero(one(X1)), one(b), zero(zero(X2))) → U81_gga(X1, X2, succcI_in_ga(X1, X2))
U81_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(zero(one(X1)), one(b), zero(zero(X2)))
addCcK_in_gga(zero(X1), one(X2), zero(X3)) → U82_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(b), zero(zero(X1)), zero(one(X1))) → U83_gga(X1, binaryZcD_in_g(X1))
U83_gga(X1, binaryZcD_out_g(X1)) → addCcK_out_gga(one(b), zero(zero(X1)), zero(one(X1)))
addCcK_in_gga(one(b), zero(one(X1)), zero(zero(X2))) → U84_gga(X1, X2, succcI_in_ga(X1, X2))
U84_gga(X1, X2, succcI_out_ga(X1, X2)) → addCcK_out_gga(one(b), zero(one(X1)), zero(zero(X2)))
addCcK_in_gga(one(X1), zero(X2), zero(X3)) → U85_gga(X1, X2, X3, addCcK_in_gga(X1, X2, X3))
addCcK_in_gga(one(X1), one(X2), one(X3)) → U86_gga(X1, X2, X3, addccH_in_gga(X1, X2, X3))
U86_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), one(X2), one(X3))
U85_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(one(X1), zero(X2), zero(X3))
U82_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addCcK_out_gga(zero(X1), one(X2), zero(X3))
U89_gga(X1, X2, X3, addCcK_out_gga(X1, X2, X3)) → addccH_out_gga(X1, X2, X3)
U74_gga(X1, X2, X3, addccH_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), one(X2), zero(X3))
U92_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addycF_out_gga(X1, X2, X3)
U73_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addzcE_out_gga(one(X1), zero(X2), one(X3))
U72_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), one(X2), one(X3))
U69_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addzcE_out_gga(zero(X1), zero(X2), zero(X3))
U63_gga(X1, X2, X3, addzcE_out_gga(X1, X2, X3)) → addcB_out_gga(zero(X1), X2, zero(X3))
addcB_in_gga(one(X1), X2, one(X3)) → U64_gga(X1, X2, X3, addycF_in_gga(X1, X2, X3))
U64_gga(X1, X2, X3, addycF_out_gga(X1, X2, X3)) → addcB_out_gga(one(X1), X2, one(X3))
U61_gga(X1, X2, X3, addcB_out_gga(X2, X4, X3)) → timescC_out_gga(one(X1), X2, X3)
U59_gga(X1, X2, X3, timescC_out_gga(X1, X2, X3)) → timescC_out_gga(zero(X1), X2, zero(X3))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timescC_in_gga(x1, x2, x3) = timescC_in_gga(x1, x2)
b = b
timescC_out_gga(x1, x2, x3) = timescC_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addcB_in_gga(x1, x2, x3) = addcB_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZcD_in_g(x1) = binaryZcD_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binarycG_in_g(x1) = binarycG_in_g(x1)
binarycG_out_g(x1) = binarycG_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZcD_out_g(x1) = binaryZcD_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addcB_out_gga(x1, x2, x3) = addcB_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzcE_in_gga(x1, x2, x3) = addzcE_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzcE_out_gga(x1, x2, x3) = addzcE_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addycF_in_gga(x1, x2, x3) = addycF_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addycF_out_gga(x1, x2, x3) = addycF_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addccH_in_gga(x1, x2, x3) = addccH_in_gga(x1, x2)
addccH_out_gga(x1, x2, x3) = addccH_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZcJ_in_ga(x1, x2) = succZcJ_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZcJ_out_ga(x1, x2) = succZcJ_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succcI_in_ga(x1, x2) = succcI_in_ga(x1)
succcI_out_ga(x1, x2) = succcI_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCcK_in_gga(x1, x2, x3) = addCcK_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCcK_out_gga(x1, x2, x3) = addCcK_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
TIMESA_IN_GGA(x1, x2, x3) = TIMESA_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESA_IN_GGA(zero(zero(X1)), X2, zero(zero(X3))) → TIMESA_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
TIMESA_IN_GGA(x1, x2, x3) = TIMESA_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMESA_IN_GGA(zero(zero(X1)), X2) → TIMESA_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

TIMESA_IN_GGA(zero(zero(X1)), X2) → TIMESA_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES